Nuprl - Proof: length le 1

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

f:(||A||||B||). Inj(||A||; ||B||; f)

By: Assert (i:||A||. j:||B||. A[i] = B[j])

Generated subgoals:

1 i:||A||. j:||B||. A[i] = B[j] 3 steps

2 6. i:||A||. j:||B||. A[i] = B[j]
f:(||A||||B||). Inj(||A||; ||B||; f) 5 steps

About: