---

Step * 2 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))
⊢ ∀as1,as2:A List.  (permutation(A;as1;as2) ⇒ (no_repeats(A;as1) ⇐⇒ no_repeats(A;as2)))
BY
{ (Auto THEN (Assert permutation(A;as2;as1) BY (RelRST THEN Auto))) }

1
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)

---

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))
\mvdash{}  \mforall{}as1,as2:A  List.    (permutation(A;as1;as2)  {}\mRightarrow{}  (no\_repeats(A;as1)  \mLeftarrow{}{}\mRightarrow{}  no\_repeats(A;as2)))


By

---

Latex:
(Auto  THEN  (Assert  permutation(A;as2;as1)  BY  (RelRST  THEN  Auto)))

---

Home Index