Nuprl - Proof: subtype-fpf-cap-void

(4steps total) PrintForm Definitions mb event system 5 Sections EventSystems Search Doc

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-void

T,X:Type, eq:EqDecider(X), f,g:x:X fp-> Type, x:X.

(f(x)?Void

r g(x)?T)

By:	Auto THEN Analyze 0 THEN All (Unfold `fpf-cap`) THEN MoveToConcl -1 THEN SplitOnConclITE THEN SplitOnConclITE

Generated subgoals:

1 1. Type
2. X : Type
3. eq : EqDecider(X)
4. f : x:X fp-> Type
5. g : x:X fp-> Type
6. x : X
7. f  g
8. x  dom(f)
9. x  dom(g)
10. x1@0 : f(x)
  x1@0  g(x)
2 steps

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. f  g
8. x  dom(f)
9. x  dom(g)
10. x1 : f(x)
  x1  T
1 step

About:

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

(4steps total) PrintForm Definitions mb event system 5 Sections EventSystems Search Doc

1	1. Type 2. X : Type 3. eq : EqDecider(X) 4. f : x:X fp-> Type 5. g : x:X fp-> Type 6. x : X 7. f g 8. x dom(f) 9. x dom(g) 10. x1@0 : f(x) x1@0 g(x)	2 steps
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. f g 8. x dom(f) 9. x dom(g) 10. x1 : f(x) x1 T	1 step