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