---

Step * 1 1 1 1 of Lemma assert-co-w-null


1. A : Type
2. w : co-w(A)
3. co-w(A) ≡ Unit + (A ⟶ co-w(A))
4. x : Unit
5. w = (inl x) ∈ (Unit + (A ⟶ co-w(A)))
6. True
⊢ (inl x) = w-nil() ∈ wfd-tree(A)
BY
{ (D (-3) THEN Fold `it` 0 THEN Fold `w-nil` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  w  :  co-w(A)
3.  co-w(A)  \mequiv{}  Unit  +  (A  {}\mrightarrow{}  co-w(A))
4.  x  :  Unit
5.  w  =  (inl  x)
6.  True
\mvdash{}  (inl  x)  =  w-nil()


By

---

Latex:
(D  (-3)  THEN  Fold  `it`  0  THEN  Fold  `w-nil`  0  THEN  Auto)

---

Home Index