---

Step * 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. z : Unit + (A ⟶ co-w(A))
5. w = z ∈ (Unit + (A ⟶ co-w(A)))
⊢ (↑co-w-null(z)) ⇒ (z = w-nil() ∈ wfd-tree(A))
BY
{ (D (-2) THEN RepUR ``co-w-null`` 0 THEN Auto) }

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

---

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{}  (\muparrow{}co-w-null(z))  {}\mRightarrow{}  (z  =  w-nil())


By

---

Latex:
(D  (-2)  THEN  RepUR  ``co-w-null``  0  THEN  Auto)

---

Home Index