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

At: length less 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. x: T
7. (x A)
8. i:
9. i < ||B||
10. x = B[i]
11. k: ||A||
(A[k] A)
By: Obvious
Generated subgoals:

None

About:
listnatural_numberless_thanuniverseequalimpliesall

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