Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
P:T
. (
x:T. Dec(P[x]))
(
f_p:T
.
x:T. P[x]
(f_p x))
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
.
f_p:T
.
x:T. P[x]
(f_p x)
T:
. P:T 
. (x:T. Dec(P[x])) 
(
f_p:T 
. x:T. P[x] 
(f_p x))f_p:T . x:T. P[x] (f_p x)