---

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


1. A : Type
2. w : co-w(A)
3. ↑co-w-null(w)
⊢ w = w-nil() ∈ wfd-tree(A)
BY
{ xxx(MoveToConcl (-1) THEN (InstLemma `co-w-ext` [⌜A⌝]⋅ THENA Auto))xxx }

1
1. A : Type
2. w : co-w(A)
3. co-w(A) ≡ Unit + (A ⟶ co-w(A))
⊢ (↑co-w-null(w)) ⇒ (w = w-nil() ∈ wfd-tree(A))

---

Latex:

---

Latex:

1.  A  :  Type
2.  w  :  co-w(A)
3.  \muparrow{}co-w-null(w)
\mvdash{}  w  =  w-nil()


By

---

Latex:
xxx(MoveToConcl  (-1)  THEN  (InstLemma  `co-w-ext`  [\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto))xxx

---

Home Index