At:
length less12
1.
T: Type
2.
A: T List
3.
B: T List
4.
no_repeats(T;A)
5.
x:T. (x A) (x B)
6.
x: T
7.
(x A)
8.
i:
9.
i < ||B||
10.
x = B[i]
11.
k: ||A||
12.
(A[k] B) j:||B||. A[k] = B[j] & j = i
By:
Analyze -1
THEN
ExRepD
THEN
InstConcl [i1]
Generated subgoal:
i1 = i
x:T. (x 
A) 
(x 
j:
