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