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