---

Step * 1 1 of Lemma co-w-null_wf


1. A : Type
2. w : co-w(A)
3. co-w(A) ≡ Unit + (A ⟶ co-w(A))
4. z : Unit + (A ⟶ co-w(A))
5. w = z ∈ (Unit + (A ⟶ co-w(A)))
⊢ co-w-null(z) ∈ 𝔹
BY
{ ProveWfLemma }

---

Latex:

---

Latex:

1.  A  :  Type
2.  w  :  co-w(A)
3.  co-w(A)  \mequiv{}  Unit  +  (A  {}\mrightarrow{}  co-w(A))
4.  z  :  Unit  +  (A  {}\mrightarrow{}  co-w(A))
5.  w  =  z
\mvdash{}  co-w-null(z)  \mmember{}  \mBbbB{}


By

---

Latex:
ProveWfLemma

---

Home Index