A1,A2:Type, B1:(A1Type), B2:(A2Type).
  strong-subtype(A1;A2)
  
  (a:A1. B1(a) r B2(a))  (a:A1 fp-> B1(a) r a:A2 fp-> B2(a))

1

1. A1 : Type 2. A2 : Type 3. B1 : A1Type 4. B2 : A2Type 5. A1 r A2 6. {b:A2| a:A1. b = a  A2 } r A1 7. a1,a2:A1. a1 = a2  A2  a1 = a2 8. a:A1. B1(a) r B2(a) 9. x : a:A1 fp-> B1(a)   x  a:A2 fp-> B2(a)

17 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html