Nuprl - Proof: one one corr fams trans

(11steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
One-to-one correspondence between indexed families of classes is transitive.

At: one one corr fams trans

A,A',A'':Type, B:(A

Type), B':(A'

Type), B'':(A''

Type).

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

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

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

By:

Auto

Generated subgoal:

1 1. A : Type
2. A' : Type
3. A'' : Type
4. B : AType
5. B' : A'Type
6. B'' : A''Type
7. (x:A. B(x)) ~ (x':A'. B'(x'))
8. (x':A'. B'(x')) ~ (x'':A''. B''(x''))
(x:A. B(x)) ~ (x'':A''. B''(x''))
10 steps

About:

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

(11steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc