A,B:Type, P:(AProp). strong-subtype(A;B)  strong-subtype({x:A| P(x) };B)

By:	Auto THEN Inst Thm* strong-subtype(A;B) Thm*  Thm* (P:(AProp), Q:(BProp). Thm* ((x:A. P(x)  Q(x))  strong-subtype({x:A| P(x) };{x:B| Q(x) })) [A;B;P;x.True] THEN ReduceSOAps 0 THEN Inst Thm* P:(AProp). strong-subtype({x:A| P(x) };A) [B;x.True]

1

1. A : Type 2. B : Type 3. P : AProp 4. strong-subtype(A;B) 5. strong-subtype({x:A| P(x) };{x:B| (x.True)(x) }) 6. strong-subtype({x:B| (x.True)(x) };B)   strong-subtype({x:A| P(x) };B)

1 step

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