---

Step * 1 of Lemma co-w-null_wf


1. A : Type
2. w : co-w(A)
3. co-w(A) ≡ Unit + (A ⟶ co-w(A))
⊢ co-w-null(w) ∈ 𝔹
BY
{ xxx(GenConcl ⌜w = z ∈ (Unit + (A ⟶ co-w(A)))⌝⋅ THEN Auto)xxx }

1
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) ∈ 𝔹

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(GenConcl  \mkleeneopen{}w  =  z\mkleeneclose{}\mcdot{}  THEN  Auto)xxx

---

Home Index