Level:
Lib
Thy
Top
:
1
2
Hypotheses:
T :
f : T
t:T. Dec(f t)
f@0:T
.
x:T. f x
(f@0 x)
Conclusion:
g:T
.
t:T. f t
(g t)
Applied Tactic:
Auto
Generated subgoals:
None
t:T. Dec(f t)
f@0:T 
. x:T. f x 
(f@0 x)
g:T . t:T. f t (g t)