PrintForm mb event system 1 Sections EventSystems Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: equal functionality wrt subtype rel
  A,B:Type, x,y:A. (A r B)  x = y  x = y  B
By: Unfold `guard` 0 THEN HypSubst -1 0 THEN Try (Fold `member` 0) THEN SubsumeC A

Generated subgoals:

None

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

PrintForm mb event system 1 Sections EventSystems Search Doc