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