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

At: length le 1 2 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)
6. f: i:||A||j:||B||A[i] = B[j]
7. a1: ||A||
8. a2: ||A||
9. j: ||B||
10. z1: A[a1] = B[j]
11. j1: ||B||
12. z2: A[a2] = B[j1]
j = j1 a1 = a2
By:
Auto
THEN
RevHypSubst -1 -2
Generated subgoal:

112. z2: A[a2] = B[j]
13. j = j1
a1 = a2		2 steps

About:
productlistnatural_numberfunctionuniverseequalimpliesall

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