(5steps total) 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: l before transitivity 1

1. T : Type
2. l : T List
3. x : T
4. y : T
5. z : T
6. no_repeats(T;l)
7. [xy l
8. [yz l
  [xz l


By: Using [`L2',[xyz]]
(BackThru Thm* L1,L2,L3:T List. L1  L2  L2  L3  L1  L3)


Generated subgoals:

1   [xz [xyz]
2 steps
2   [xyz l
1 step

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

(5steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc