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

At: no repeats append iff
T:Type, l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2)
By: Unfolds [`no_repeats`;`l_disjoint`] 0
Generated subgoals:

11. T: Type
2. l1: T List
3. l2: T List
4. i,j:. i < ||l1 @ l2|| j < ||l1 @ l2|| i = j (l1 @ l2)[i] = (l1 @ l2)[j]
5. x: T
((x l1) & (x l2))		3 steps
 
21. T: Type
2. l1: T List
3. l2: T List
4. i,j:. i < ||l1 @ l2|| j < ||l1 @ l2|| i = j (l1 @ l2)[i] = (l1 @ l2)[j]
5. i:
6. j:
7. i < ||l1||
8. j < ||l1||
9. i = j
l1[i] = l1[j]		1 step
 
31. T: Type
2. l1: T List
3. l2: T List
4. i,j:. i < ||l1 @ l2|| j < ||l1 @ l2|| i = j (l1 @ l2)[i] = (l1 @ l2)[j]
5. i:
6. j:
7. i < ||l2||
8. j < ||l2||
9. i = j
l2[i] = l2[j]		1 step
 
41. T: Type
2. l1: T List
3. l2: T List
4. x:T. ((x l1) & (x l2))
5. i,j:. i < ||l1|| j < ||l1|| i = j l1[i] = l1[j]
6. i,j:. i < ||l2|| j < ||l2|| i = j l2[i] = l2[j]
7. i:
8. j:
9. i < ||l1 @ l2||
10. j < ||l1 @ l2||
11. i = j
(l1 @ l2)[i] = (l1 @ l2)[j]		7 steps

About:
listuniverseequalandall

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