(6steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
At:
decidable
iff
exists
bool
function
T:Type, P:(T
Prop). (
x:T. Dec(P(x)))
(
f_p:(T
).
x:T. P(x)
f_p(x))
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
P:
T
Prop
3.
x:T. Dec(P(x))
f_p:(T
).
x:T. P(x)
f_p(x)
About:
(6steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
Prop
x:T. Dec(P(x))
f_p:(T
). x:T. P(x) 
f_p(x)
T:Type, P:(TProp). (x:T. Dec(P(x))) 
(f_p:(T). x:T. P(x) f_p(x))
Propx:T. Dec(P(x)) f_p:(T). x:T. P(x) f_p(x)
