C,A,B:T List. C 
A @ B 
(
A',B':T List. C = (A' @ B') & A' A & B' B) L2 == f:(
||L1||
||L2||). increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))] 
T)
is mentioned by
| Thm* C,A,B:T List. C A @ B (A',B':T List. C = (A' @ B') & A' A & B' B) | [sublist_append_iff] |
In prior sections: mb list 1 mb list 2
Try larger context:
Graphs