Level:
Lib
Thy
Top
:
1
1
Hypotheses:
n : {1...}
m :
n
E :
n
n
Sym(
n;x,y.x E y)
a :
m
Conclusion:
b:
m. a E b
b E a
Applied Tactic:
(Unfold `sym` 4 THENM D 0 ...a)
Generated subgoals:
1
. a E b
b E a
nn 
n 
n;x,y.x E y)m
b:m. a E b 
b E a b E a