Nuprl - Proof: length le 1 2

(10steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: length le 1 2

1. T: Type
2. A: T List
3. B: T List
4. no_repeats(T;A)
5. x:T. (x A) (x B)
6. i:||A||. j:||B||. A[i] = B[j]

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

By: RenameVar `f' -1 THEN Unfolds [`all`;`exists`] -1 THEN InstConcl [i.1of(f(i))] THEN Unfold `inject` 0 THEN Reduce 0 THEN RepeatFor 2 (Analyze 0)

Generated subgoal:

1 6. f: i:||A||j:||B||A[i] = B[j]
7. a1: ||A||
8. a2: ||A||
1of(f(a1)) = 1of(f(a2)) a1 = a2 4 steps

About:

(10steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc