A,B:Type. strong-subtype(A;B)  (L:A List, x:B. (x  L)  x  A)

By:	Auto THEN AssertBY (A r B) (Unfold `strong-subtype` 3 THEN ExRepD) THEN AssertBY A  B (Analyze 0 THEN DoSubsume) THEN TrySubsume

1

1. A : Type 2. B : Type 3. strong-subtype(A;B) 4. L : A List 5. x : B 6. (x  L) 7. A r B 8. A  B   x  A

3 steps

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