Nuprl Basics - Proof: sfa doc exteq gfun

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc exteq gfun

A:Type, B:(A

Prop), C:({u:A| B(u) }

Type).

x:{u:A| B(u) }

C(x) =ext x:A

C(x)(given B(x))

By:

UnivCD

Generated subgoal:

1 1. A : Type
2. B : AProp
3. C : {u:A| B(u) }Type
x:{u:A| B(u) }C(x) =ext x:AC(x)(given B(x))
7 steps

About:

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