(4steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nil interleaving2
  T:Type, L1,L:T List. interleaving(T;L1;nil;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|| = ||L1||+0  
5. disjoint_sublists(T;L1;nil;L)
  L = L1
2 steps
2 1. T : Type
2. L1 : T List
3. L : T List
4. L = L1
  disjoint_sublists(T;L1;nil;L1)
1 step

About:
listniluniverseequalall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

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