---

Step * of Lemma permutation-rotate-cons

∀[A:Type]. ∀a:A. ∀as:A List.  permutation(A;[a / as];as @ [a])
BY
{ (Auto THEN (InstLemma `permutation-rotate` [⌜A⌝;⌜[a]⌝;⌜as⌝]⋅ THENA Auto) THEN Reduce (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}a:A.  \mforall{}as:A  List.    permutation(A;[a  /  as];as  @  [a])


By

---

Latex:
(Auto  THEN  (InstLemma  `permutation-rotate`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}[a]\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Reduce  (-1)  THEN  Auto)

---

Home Index