A,A',B,B':Type. (A ~ A')  (B ~ B')  ((A inj B) ~ (A' inj B'))

1

1. A : Type 2. A' : Type 3. B : Type 4. B' : Type 5. A ~ A' 6. B ~ B'   (A inj B) ~ (A' inj B')

13 steps

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