Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
. Discrete{T}
(
f:{T=
}. True)
Applied Tactic:
D 0 THENA Auto
Generated subgoals:
1
. Discrete{T}
(
f:{T=
}. True)
T:
. Discrete{T} 
(
f:{T=
}. True) (f:{T=}. True)