Nuprl - Proof: subtype-fpf-cap-top 2

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: subtype-fpf-cap-top 2

1. T : Type
2. X : Type
3. eq : EqDecider(X)
4. f : x:X fp-> Type
5. g : x:X fp-> Type
6. x : X
7. g

f
8.

dom(f)
9. x

dom(g)
10. x1@0 : T

x1@0

g(x)

By:	Unfold `fpf-sub` -4 THEN InstHyp [x] -4 THEN ExRepD

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html