A,B:Type, d:EqDecider(B). strong-subtype(A;B)  d  EqDecider(A)

1

1. A : Type 2. B : Type 3. d : EqDecider(B) 4. A r B 5. {b:B| a:A. b = a  B } r A 6. a1,a2:A. a1 = a2  B  a1 = a2   d  EqDecider(A)

6 steps

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