Nuprl - Proof: union functionality wrt one one corr 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: union functionality wrt one one corr 1 1

1. A : Type
2. A' : Type
3. B : Type
4. B' : Type
5. f : A

A'
6. g : A'

A
7. InvFuns(A;A';f;g)
8. f1 : B

B'
9. g1 : B'

B
10. InvFuns(B;B';f1;g1)

InvFuns(A+B;A'+B'

InvFuns;

z.InjCase(z; x. inl(f(x)); y. inr(f1(y)))

InvFuns;

z.InjCase(z; x. inl(g(x)); y. inr(g1(y))))

By:	Analyze THEN Analyze-1 THEN Reduce Concl THEN Analyze

Generated subgoals:

1 11. x1 : A
  g(f(x1)) = x1
1 step

2 11. y : B
  g1(f1(y)) = y
1 step

3 11. x : A'
  f(g(x)) = x
1 step

4 11. y1 : B'
  f1(g1(y1)) = y1
1 step

About:

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