1. A : Type
2. A' : Type
3. strong-subtype(A;A')
4. B : AType
5. C : A'Type
6. eq : EqDecider(A)
7. eq' : EqDecider(A')
8. f : a:A fp-> B(a)
9. g : a:A fp-> B(a)
10. A r A'
11. eq'  EqDecider(A)
12. a:A. B(a) r C(a)
13. x:A. x  dom(f)  x  dom(g) & f(x) = g(x)
14. x : A
  x  dom(f)  Prop{1}

By:	Auto THEN DoSubsume THEN BackThru Thm* B1:(A1Type), B2:(A2Type). Thm* strong-subtype(A1;A2) Thm*  Thm* (a:A1. B1(a) r B2(a))  (a:A1 fp-> B1(a) r a:A2 fp-> B2(a)) THEN Analyze 0

None

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