---

Step * of Lemma no_repeats_append

∀[T:Type]. ∀[l1,l2:T List].  l_disjoint(T;l1;l2) supposing no_repeats(T;l1 @ l2)
BY
{ ((((Unfolds ``no_repeats l_disjoint`` 0 THEN Auto) THEN D 0) THENA Auto) THEN Unfold `l_member` (-1) THEN ExRepD) }

1
1. T : Type
2. l1 : T List
3. l2 : T List
4. ∀[i,j:ℕ].  (¬(l1 @ l2[i] = l1 @ l2[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||l1 @ l2|| and i < ||l1 @ l2||)
5. x : T
6. i1 : ℕ
7. i1 < ||l1||
8. x = l1[i1] ∈ T
9. i : ℕ
10. i < ||l2||
11. x = l2[i] ∈ T
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l1,l2:T  List].    l\_disjoint(T;l1;l2)  supposing  no\_repeats(T;l1  @  l2)


By

---

Latex:
((((Unfolds  ``no\_repeats  l\_disjoint``  0  THEN  Auto)  THEN  D  0)  THENA  Auto)
  THEN  Unfold  `l\_member`  (-1)
  THEN  ExRepD)

---

Home Index