Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
n:{1...}.
m:
n.
E:
n
n
. Sym(
n;x,y.x E y)
Sym(
m;x,y.x E y)
Applied Tactic:
(UnivCD ...a)
Generated subgoals:
1
. Sym(
m;x,y.x E y)
n:{1...}. m:
n. E:n 
n 
. Sym(n;x,y.x E y) 
Sym(m;x,y.x E y)m;x,y.x E y)