---

Step * 1 of Lemma no_repeats_functionality_wrt_permutation

.....assertion..... 
1. A : Type
⊢ ∀as1,as2:A List.  (permutation(A;as1;as2) ⇒ no_repeats(A;as1) ⇒ no_repeats(A;as2))
BY
{ (Auto THEN D -2 THEN Auto THEN HypSubst' -2 0 THEN Auto THEN ParallelLast) }

1
1. A : Type
2. as1 : A List
3. as2 : A List
4. f : ℕ||as1|| ⟶ ℕ||as1||
5. Inj(ℕ||as1||;ℕ||as1||;f)
6. as2 = (as1 o f) ∈ (A List)
7. ∀[i,j:ℕ].  (¬(as1[i] = as1[j] ∈ A)) supposing ((¬(i = j ∈ ℕ)) and j < ||as1|| and i < ||as1||)
⊢ ∀[i,j:ℕ].  (¬((as1 o f)[i] = (as1 o f)[j] ∈ A)) supposing ((¬(i = j ∈ ℕ)) and j < ||(as1 o f)|| and i < ||(as1 o f)||)

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
\mvdash{}  \mforall{}as1,as2:A  List.    (permutation(A;as1;as2)  {}\mRightarrow{}  no\_repeats(A;as1)  {}\mRightarrow{}  no\_repeats(A;as2))


By

---

Latex:
(Auto  THEN  D  -2  THEN  Auto  THEN  HypSubst'  -2  0  THEN  Auto  THEN  ParallelLast)

---

Home Index