Nuprl Basics - Proof: sfa doc exteq gprop

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

A:Type, P:(A

Prop). {x:A| P(x) }

Prop =ext x:A

Prop(given P(x))

By:

UnivCD

Generated subgoal:

1 1. A : Type
2. P : AProp
{x:A| P(x) }Prop =ext x:AProp(given P(x))
5 steps

About:

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