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: subtype rel transitivity

  A,B,C:Type. (A B (B C (A C)

By: Auto THEN Analyze 0 THEN SubsumeC B THEN SubsumeC A


Generated subgoals:

None

About:
universesubtype_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