(4steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nil interleaving
  T:Type, L1,L:T List. interleaving(T;nil;L1;L)  L = L1
By: Unfold `interleaving` 0 THEN Reduce 0 THEN Try (WeakSubstFor L 0)

Generated subgoals:

1 1. T : Type
2. L1 : T List
3. L : T List
4. ||L|| = 0+||L1||  
5. disjoint_sublists(T;nil;L1;L)
  L = L1
2 steps
2 1. T : Type
2. L1 : T List
3. L : T List
4. L = L1
  disjoint_sublists(T;nil;L1;L1)
1 step

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

(4steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc