Level:
Lib
Thy
Top
:
1
Hypotheses:
T :
f : T
t:T. Dec(f t)
Conclusion:
g:T
.
t:T. f t
(g t)
Applied Tactic:
InstLemma `ax_choice` [
T
;
;
t b.f t
b
] THENW Auto
Generated subgoals:
1
.
x:T.
y:
. f x
y
2
.
g:T
.
t:T. f t
(g t)
t:T. Dec(f t)
g:T 
. t:T. f t 
(g t)
T
;;
t b.f t b] THENW Autox:T. y:. f x yg:T . t:T. f t (g t)