---

Step * 1 of Lemma squash-list-exists


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]]))
BY
{ (D 0 THEN With ⌜[]⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  R  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}i:\mBbbN{}0.  (\mdownarrow{}\mexists{}b:B.  R[\mbot{};b])
\mvdash{}  \mdownarrow{}\mexists{}bs:B  List.  ((||bs||  =  0)  \mwedge{}  (\mforall{}i:\mBbbN{}0.  R[\mbot{};bs[i]]))


By

---

Latex:
(D  0  THEN  With  \mkleeneopen{}[]\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index