---

Step * of Lemma squash-list-exists

∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
  ∀as:A List
    ((∀i:ℕ||as||. (↓∃b:B. R[as[i];b])) ⇒ (↓∃bs:B List. ((||bs|| = ||as|| ∈ ℤ) ∧ (∀i:ℕ||as||. R[as[i];bs[i]]))))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }

1
1. A : Type
2. B : Type
3. R : A ⟶ B ⟶ ℙ
4. ∀i:ℕ0. (↓∃b:B. R[⊥;b])
⊢ ↓∃bs:B List. ((||bs|| = 0 ∈ ℤ) ∧ (∀i:ℕ0. R[⊥;bs[i]]))

2
1. A : Type
2. B : Type
3. R : A ⟶ B ⟶ ℙ
4. u : A
5. v : A List
6. (∀i:ℕ||v||. (↓∃b:B. R[v[i];b])) ⇒ (↓∃bs:B List. ((||bs|| = ||v|| ∈ ℤ) ∧ (∀i:ℕ||v||. R[v[i];bs[i]])))
7. ∀i:ℕ||v|| + 1. (↓∃b:B. R[[u / v][i];b])
⊢ ↓∃bs:B List. ((||bs|| = (||v|| + 1) ∈ ℤ) ∧ (∀i:ℕ||v|| + 1. R[[u / v][i];bs[i]]))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}as:A  List
        ((\mforall{}i:\mBbbN{}||as||.  (\mdownarrow{}\mexists{}b:B.  R[as[i];b]))
        {}\mRightarrow{}  (\mdownarrow{}\mexists{}bs:B  List.  ((||bs||  =  ||as||)  \mwedge{}  (\mforall{}i:\mBbbN{}||as||.  R[as[i];bs[i]]))))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index