---

Step * 1 1 1 1 of Lemma wfd-tree-cases


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index