---

Step * 1 of Lemma no_repeats-permute

.....assertion..... 
∀T:Type. ∀as,bs:T List.  (no_repeats(T;as @ bs) ⇒ no_repeats(T;bs @ as))
BY
{ xxx(Unfold `no_repeats` 0 THEN Auto)xxx }

1
1. T : Type
2. as : T List
3. bs : T List
4. ∀[i,j:ℕ].  (¬(as @ bs[i] = as @ bs[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||as @ bs|| and i < ||as @ bs||)
5. i : ℕ
6. j : ℕ
7. i < ||bs @ as||
8. j < ||bs @ as||
9. ¬(i = j ∈ ℕ)
⊢ ¬(bs @ as[i] = bs @ as[j] ∈ T)

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}T:Type.  \mforall{}as,bs:T  List.    (no\_repeats(T;as  @  bs)  {}\mRightarrow{}  no\_repeats(T;bs  @  as))


By

---

Latex:
xxx(Unfold  `no\_repeats`  0  THEN  Auto)xxx

---

Home Index