---

Step * of Lemma assert-co-w-null

∀[A:Type]. ∀[w:co-w(A)].  uiff(↑co-w-null(w);w = w-nil() ∈ co-w(A))
BY
{ xxx(Auto THEN Try ((SubsumeC ⌜wfd-tree(A)⌝⋅ THEN Auto)) THEN Try ((HypSubst (-1) 0 THEN Auto)))xxx }

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

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[w:co-w(A)].    uiff(\muparrow{}co-w-null(w);w  =  w-nil())


By

---

Latex:
xxx(Auto  THEN  Try  ((SubsumeC  \mkleeneopen{}wfd-tree(A)\mkleeneclose{}\mcdot{}  THEN  Auto))  THEN  Try  ((HypSubst  (-1)  0  THEN  Auto)))xxx

---

Home Index