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 append
  T:Type, l1,l2,l3:T List. l1  l2  l1  l2 @ l3
By: Unfold `iseg` 0 THEN ExRepD THEN InstConcl [l @ l3] THEN WeakSubstFor l2 0
THEN
RWO Thm* as,bs,cs:T List. ((as @ bs) @ cs) = (as @ (bs @ cs)) 0

Generated subgoals:

None

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

PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc