Level:
Lib
Thy
Top
:
1
1
Hypotheses:
n : {1...}
m :
n
E :
n
n
Trans(
n;x,y.x E y)
a :
m
Conclusion:
b,c:
m. a E b
b E c
a E c
Applied Tactic:
(UnivCD THENM Unfold `trans` 4 ...a)
Generated subgoals:
1
. a E c
nn 
n 
n;x,y.x E y)m
b,c:m. a E b 
b E c a E c