Nuprl - Proof: union functionality wrt one one corr 1

(7steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

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

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

f:(A

A'), g:(A'

A). InvFuns(A;A';f;g)
6.

f:(B

B'), g:(B'

B). InvFuns(B;B';f;g)

f:((A+B)

(A'+B')), g:((A'+B')

(A+B)). InvFuns(A+B;A'+B';f;g)

By:	2 Times Analyze-2 THEN 2 Times Analyze-1 THEN Witness: Wiz.InjCase(z; x. inl(f(x)); y. inr(f1(y))) \| Wiz.InjCase(z; x. inl(g(x)); y. inr(g1(y)))

Generated subgoal:

1 5. f : AA'
6. g : A'A
7. InvFuns(A;A';f;g)
8. f1 : BB'
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))))
5 steps

About:

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

(7steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc