Nuprl - Proof: strong-subtype-deq-subtype

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: strong-subtype-deq-subtype

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

(EqDecider(B)

r EqDecider(A))

By:	Auto THEN Analyze 0 THEN BackThru Thm* d:EqDecider(B). strong-subtype(A;B) d EqDecider(A)

Generated subgoals:

None

About:

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