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