---

Step * 1 of Lemma filter-index_wf


1. T : Type
2. P : T ⟶ 𝔹
3. i : ℕ0
⊢ (↑(P ⊥)) ⇒ (filter-index(P;[]) i ∈ {j:ℕ0| ⊥ = ⊥ ∈ T} )
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  i  :  \mBbbN{}0
\mvdash{}  (\muparrow{}(P  \mbot{}))  {}\mRightarrow{}  (filter-index(P;[])  i  \mmember{}  \{j:\mBbbN{}0|  \mbot{}  =  \mbot{}\}  )


By

---

Latex:
Auto

---

Home Index