---

Step * of Lemma no_repeats_functionality_wrt_permutation

∀[A:Type]. ∀as1,as2:A List.  (permutation(A;as1;as2) ⇒ (no_repeats(A;as1) ⇐⇒ no_repeats(A;as2)))
BY
{ ((D 0 THENA Auto)
   THEN Assert ⌜∀as1,as2:A List.  (permutation(A;as1;as2) ⇒ no_repeats(A;as1) ⇒ no_repeats(A;as2))⌝⋅
   ) }

1
.....assertion..... 
1. A : Type
⊢ ∀as1,as2:A List.  (permutation(A;as1;as2) ⇒ no_repeats(A;as1) ⇒ no_repeats(A;as2))

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

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}as1,as2:A  List.    (permutation(A;as1;as2)  {}\mRightarrow{}  (no\_repeats(A;as1)  \mLeftarrow{}{}\mRightarrow{}  no\_repeats(A;as2)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  Assert  \mkleeneopen{}\mforall{}as1,as2:A  List.    (permutation(A;as1;as2)  {}\mRightarrow{}  no\_repeats(A;as1)  {}\mRightarrow{}  no\_repeats(A;as2))\mkleeneclose{}\mcdot{}
  )

---

Home Index