Level:
Lib
Thy
Top
:
1
Hypotheses:
n : {1...}
m :
n
E :
n
n
Trans(
n;x,y.x E y)
Conclusion:
Trans(
m;x,y.x E y)
Applied Tactic:
(D 0 ...a)
Generated subgoals:
1
.
b,c:
m. a E b
b E c
a E c
nn 
n 
n;x,y.x E y)
Trans(m;x,y.x E y)
b,c:m. a E b 
b E c a E c