Nuprl - Proof: bijtype exteq inj isect surjtype 1 2 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bijtype exteq inj isect surjtype 1 2 1 1 1 1

1. A : Type
2. B : Type
3. x :
3.

2. if i=

{f:(A

B)| Inj(A; B; f) } else {f:(A

B)| Surj(A; B; f) } fi
4. 0

2
5. y : {f:(A

B)| Inj(A; B; f) }
6. y = x
7. Inj(A; B; y)
8. 1

2
9. y1 : {f:(A

B)| Surj(A; B; f) }
10. y1 = x
11. Surj(A; B; y1)

Inj(A; B; x)

By:	Rewrite by y = x AB

Generated subgoals:

None

About:

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