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