Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
eq:{T
}.
x,y:T.
(eq x y)
(eq y x)
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
.
(eq x y)
(eq y x)
T:
. eq:{T
}. x,y:T. 
(eq x y) 
(eq y x)(eq x y) (eq y x)