Nuprl - Proof: fpf-dom-type

(5steps total) PrintForm Definitions Lemmas mb event system 3 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: fpf-dom-type

X,Y:Type, eq:EqDecider(Y), f:x:X fp-> Top, x:Y.

strong-subtype(X;Y)

dom(f)

By:

Auto

Generated subgoals:

1 1. X : Type
2. Y : Type
3. eq : EqDecider(Y)
4. f : x:X fp-> Top
5. x : Y
6. strong-subtype(X;Y)
7. x  dom(f)
  x  X
3 steps

2 1. X : Type
2. Y : Type
3. EqDecider(Y)
4. f : x:X fp-> Top
5. Y
6. strong-subtype(X;Y)
  f  a:Y fp-> Top
1 step

About:

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

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

1	1. X : Type 2. Y : Type 3. eq : EqDecider(Y) 4. f : x:X fp-> Top 5. x : Y 6. strong-subtype(X;Y) 7. x dom(f) x X	3 steps
2	1. X : Type 2. Y : Type 3. EqDecider(Y) 4. f : x:X fp-> Top 5. Y 6. strong-subtype(X;Y) f a:Y fp-> Top	1 step