PrintForm
Definitions
mb
list
2
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
interleaving
sublist
T
:Type,
L
,
L1
,
L2
:
T
List. interleaving(
T
;
L1
;
L2
;
L
)
L1
L
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 /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
list
2
Sections
MarkB
generic
Doc
T:Type, L,L1,L2:T List. interleaving(T;L1;L2;L) 
L1 
L T:Type, L,L1,L2:T List. interleaving(T;L1;L2;L) L1 L
