gen2

Theorem.

Arguments:

x (sv), y (sv), phi (pr),

Hypotheses:

phi

Assertions:

forallxforallyphi

Proof:

Hyp Ref Line Expr
Hypo1phi
1ax-gen2forallyphi
2ax-gen3forallxforallyphi