X,Y:Type, eq:EqDecider(Y), f:x:X fp-> Top, x:Y.
  strong-subtype(X;Y)  x  dom(f)  x  X

By:	Unfold `guard` 0 THEN Inst Thm* eq:EqDecider(Y), f:x:X fp-> Top, x:Y. Thm* strong-subtype(X;Y)  x  dom(f)  x  X [] THEN Trivial

None

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