IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
interleaving sublist T:Type, L,L1,L2:T List. interleaving(T;L1;L2;L) L1L
By:
Unfolds [`interleaving`;`sublist`] 0 THEN Unfold `disjoint_sublists` 0
THEN
ExRepD
THEN
InstConcl [f1]
THEN
EasyHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
T:Type, L,L1,L2:T List. interleaving(T;L1;L2;L) 
L1 
L
