Nuprl Basics - Proof: sfa doc bool vs decidable fun

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc bool vs decidable fun

A:Type, P:(A

Prop). (

x:A. Dec(P(x)))

(

f:(A

x:A. P(x)

f(x))

By:

Auto

Generated subgoal:

1 1. A : Type
2. P : AProp
3. x:A. Dec(P(x))
f:(A). x:A. P(x) f(x)
2 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html