Nuprl - Proof: one one corr fams sym 1

(15steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one one corr fams sym 1

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

Type
4. B' : A'

Type
5. (x:A. B(x)) ~ (x':A'. B'(x'))

(x':A'. B'(x')) ~ (x:A. B(x))

By:	(-1) Def THEN ExistHD Hyp:5

Generated subgoal:

1 5. f : AA'
6. g : A'A
7. F : x:AB(x)B'(f(x))
8. G : x:AB'(f(x))B(x)
9. InvFuns(A;A';f;g)
10. u:A. InvFuns(B(u);B'(f(u));F(u);G(u))
(x':A'. B'(x')) ~ (x:A. B(x))
13 steps

About:

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

(15steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc