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