PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: iseg transitivity2
  T:Type, l1,l2,l3:T List. l2  l3  l1  l2  l1  l3
By: Auto THEN Inst Thm* l1,l2,l3:T List. l1  l2  l2  l3  l1  l3 [T;l1;l2;l3]

Generated subgoals:

None

About:
listuniverseimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc