---

Step * 2 1 of Lemma no_repeats_functionality_wrt_permutation


1. A : Type
2. ∀as1,as2:A List.  (permutation(A;as1;as2) ⇒ no_repeats(A;as1) ⇒ no_repeats(A;as2))
3. as1 : A List
4. as2 : A List
5. permutation(A;as1;as2)
6. no_repeats(A;as2)
7. permutation(A;as2;as1)
⊢ no_repeats(A;as1)
BY
{ Auto }

---

Latex:

---

Latex:

1.  A  :  Type
2.  \mforall{}as1,as2:A  List.    (permutation(A;as1;as2)  {}\mRightarrow{}  no\_repeats(A;as1)  {}\mRightarrow{}  no\_repeats(A;as2))
3.  as1  :  A  List
4.  as2  :  A  List
5.  permutation(A;as1;as2)
6.  no\_repeats(A;as2)
7.  permutation(A;as2;as1)
\mvdash{}  no\_repeats(A;as1)


By

---

Latex:
Auto

---

Home Index