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

At: length le 1 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||
7. (A[i] B)
j:||B||. A[i] = B[j]
By:
Analyze -1
THEN
Obvious
Generated subgoals:

None

About:
listnatural_numberuniverseequalimpliesallexists

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