L1,L2,L:T List, x:T.
Thm* no_repeats(T;L)
L1 @ [x] 
L [x / L2] L L1 @ [x / L2] Lk:
, f:(k
). increasing(f;k) (x,y:k. x<y f(x)<f(y))as,bs:T List. ||as @ bs|| = ||as||+||bs|| 
as,bs:T List, i:||as||. (as @ bs)[i] = as[i]as,bs:T List, i:{||as||..(||as||+||bs||)
}. (as @ bs)[i] = bs[(i-||as||)]