Nuprl - Proof: length le 1 1

At: length le 1 1

1. T: Type
2. A: T List
3. B: T List
4. no_repeats(T;A)
5. x:T. (x A) (x B)

i:||A||. j:||B||. A[i] = B[j]

By: Analyze 0 THEN InstHyp [A[i]] -2

Generated subgoals:

1 6. i: ||A||
(A[i] A) 1 step

2 6. i: ||A||
7. (A[i] B)
j:||B||. A[i] = B[j] 1 step

About: