---

Step * 1 2 1 of Lemma cons_cancel_wrt_permutation


1. [A] : Type
2. a : A
3. bs : A List
4. cs : A List
5. ||[a / bs]|| = ||[a / cs]|| ∈ ℤ
6. ||bs|| = ||cs|| ∈ ℤ
7. g : ℕ||[a / bs]|| ⟶ ℕ||[a / bs]||
8. Inj(ℕ||[a / bs]||;ℕ||[a / bs]||;g)
9. [a / cs] = ([a / bs] o g) ∈ (A List)
10. (g 0) = 0 ∈ ℤ
⊢ ∃f:ℕ||bs|| ⟶ ℕ||bs||. (Inj(ℕ||bs||;ℕ||bs||;f) ∧ (cs = (bs o f) ∈ (A List)))
BY
{ (Assert 0 < ||[a / bs]|| BY
         Auto') }

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

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  a  :  A
3.  bs  :  A  List
4.  cs  :  A  List
5.  ||[a  /  bs]||  =  ||[a  /  cs]||
6.  ||bs||  =  ||cs||
7.  g  :  \mBbbN{}||[a  /  bs]||  {}\mrightarrow{}  \mBbbN{}||[a  /  bs]||
8.  Inj(\mBbbN{}||[a  /  bs]||;\mBbbN{}||[a  /  bs]||;g)
9.  [a  /  cs]  =  ([a  /  bs]  o  g)
10.  (g  0)  =  0
\mvdash{}  \mexists{}f:\mBbbN{}||bs||  {}\mrightarrow{}  \mBbbN{}||bs||.  (Inj(\mBbbN{}||bs||;\mBbbN{}||bs||;f)  \mwedge{}  (cs  =  (bs  o  f)))


By

---

Latex:
(Assert  0  <  ||[a  /  bs]||  BY
              Auto')

---

Home Index