At:
no repeats append iff
1
1
1
1.
T: Type
2.
l1: T List
3.
l2: T List
4.
i,j:
. i < ||l1||+||l2|| 
j < ||l1||+||l2|| 
i = j (l1 @ l2)[i] = (l1 @ l2)[j]
5.
x: T
6.
i1:
7.
i1 < ||l1||
8.
x = l1[i1]
9.
i:
10.
i < ||l2||
11.
x = l2[i]
l1[i1] = l2[(i+||l1||-||l1||)]
By:
Obvious
Generated subgoals:
None
About:
