Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
f:T
. (
t:T. Dec(f t))
(
g:T
.
t:T. f t
(g t))
Applied Tactic:
UnivCD THENW Auto
Generated subgoals:
1
.
g:T
.
t:T. f t
(g t)
T:
. f:T 
. (t:T. Dec(f t)) 
(
g:T 
. t:T. f t 
(g t))g:T . t:T. f t (g t)