Nuprl Basics - Proof: sfa doc exteq gfun 1

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

1. A : Type
2. B : A

Prop
3. C : {u:A| B(u) }

Type

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

C(x) =ext x:A

C(x)(given B(x))

By:	Analyze THEN New:f Analyze THEN FunExtensionality

Generated subgoals:

1 4. f : x:{u:A| B(u) }C(x)
5. x : A
f(x) C(x)(given B(x))
3 steps

2 4. f : x:AC(x)(given B(x))
5. x : {u:A| B(u) }
f(x) C(x)
3 steps

About:

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

1	4. f : x:{u:A\| B(u) }C(x) 5. x : A f(x) C(x)(given B(x))	3 steps
2	4. f : x:AC(x)(given B(x)) 5. x : {u:A\| B(u) } f(x) C(x)	3 steps