Inference at * 1 2 2 2 1 
Iof proof for Lemma append overlapping sublists:

.....truecase..... NILNIL

1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6. i, j:. (i < ||L||)  (j < ||L||)  ((i = j))  ((L[i] = L[j]))
7. f1 : {0..||L1 @ [x]||}{0..||L||}
8. increasing(f1;||L1 @ [x]||)
9. j:{0..||L1 @ [x]||}. (L1 @ [x])[j] = L[(f1(j))]
10. f : {0..(||L2||+1)}{0..||L||}
11. increasing(f;||L2||+1)
12. j:{0..(||L2||+1)}. [x / L2][j] = L[(f(j))]
13. ||L1 @ [x / L2]|| = ||L1||+||L2||+1
14. ||[]||  0 
15. j : {0..||L1 @ [x / L2]||}
16. ||L1 @ [x]|| = ||L1||+1
17. j  ||L1||
  (L1 @ [x / L2])[j] = L[(f1(j))] 

latex

 by ((Decide j = ||L1||) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok SupInf:t) inil_term))) 

latex

C1: 

C1: 18. j = ||L1||
C1:   (L1 @ [x / L2])[j] = L[(f1(j))]
C2: 

C2: 18. (j = ||L1||)
C2:   (L1 @ [x / L2])[j] = L[(f1(j))]
C.

Definitions	t  T, P  Q, Dec(P), {i..j}, x:A. B(x)
Lemmas	length wf1, decidable int equal