---

Step * of Lemma permutation_functionality_wrt_permutation

∀[A:Type]
  ∀as1,as2,bs1,bs2:A List.
    (permutation(A;as1;as2) ⇒ permutation(A;bs1;bs2) ⇒ (permutation(A;as1;bs1) ⇐⇒ permutation(A;as2;bs2)))
BY
{ (Auto THEN RelRST THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RelRST  THEN  Auto)

---

Home Index