---

Step * of Lemma cons_cancel_wrt_permutation

No Annotations
∀[A:Type]. ∀a:A. ∀bs,cs:A List.  (permutation(A;[a / bs];[a / cs]) ⇒ permutation(A;bs;cs))
BY
{ (Auto
   THEN (FLemma `permutation-length` [-1] THENA Auto)
   THEN (Assert ||bs|| = ||cs|| ∈ ℤ BY
               Auto')
   THEN All
   (Unfold `permutation`)⋅
   THEN ExRepD) }

1
1. [A] : Type
2. a : A
3. bs : A List
4. cs : A List
5. f : ℕ||[a / bs]|| ⟶ ℕ||[a / bs]||
6. Inj(ℕ||[a / bs]||;ℕ||[a / bs]||;f)
7. [a / cs] = ([a / bs] o f) ∈ (A List)
8. ||[a / bs]|| = ||[a / cs]|| ∈ ℤ
9. ||bs|| = ||cs|| ∈ ℤ
⊢ ∃f:ℕ||bs|| ⟶ ℕ||bs||. (Inj(ℕ||bs||;ℕ||bs||;f) ∧ (cs = (bs o f) ∈ (A List)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}a:A.  \mforall{}bs,cs:A  List.    (permutation(A;[a  /  bs];[a  /  cs])  {}\mRightarrow{}  permutation(A;bs;cs))


By

---

Latex:
(Auto
  THEN  (FLemma  `permutation-length`  [-1]  THENA  Auto)
  THEN  (Assert  ||bs||  =  ||cs||  BY
                          Auto')
  THEN  All
  (Unfold  `permutation`)\mcdot{}
  THEN  ExRepD)

---

Home Index