---

Step * of Lemma permutation-invariant

∀[T:Type]. ∀[P:(T List) ⟶ ℙ].
  ((∀as:T List. ∀a:T.  (P[[a / as]] ⇒ P[as @ [a]]))
  ⇒ (∀as:T List. ∀a1,a2:T.  (P[[a1; [a2 / as]]] ⇒ P[[a2; [a1 / as]]]))
  ⇒ (∀as,bs:T List.  (permutation(T;as;bs) ⇒ (P[as] ⇐⇒ P[bs]))))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN InstLemma `permutation-invariant2` [⌜T⌝;⌜λ2as bs.P[as] ⇒ P[bs]⌝]⋅
   THEN Auto
   THEN Try ((D 0 THEN Auto))
   THEN FLemma `permutation_inversion` [-2]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}as:T  List.  \mforall{}a:T.    (P[[a  /  as]]  {}\mRightarrow{}  P[as  @  [a]]))
    {}\mRightarrow{}  (\mforall{}as:T  List.  \mforall{}a1,a2:T.    (P[[a1;  [a2  /  as]]]  {}\mRightarrow{}  P[[a2;  [a1  /  as]]]))
    {}\mRightarrow{}  (\mforall{}as,bs:T  List.    (permutation(T;as;bs)  {}\mRightarrow{}  (P[as]  \mLeftarrow{}{}\mRightarrow{}  P[bs]))))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  InstLemma  `permutation-invariant2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}as  bs.P[as]  {}\mRightarrow{}  P[bs]\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((D  0  THEN  Auto))
  THEN  FLemma  `permutation\_inversion`  [-2]
  THEN  Auto)

---

Home Index