---

Step * of Lemma wfd-tree-cases

∀[A:Type]
  ∀w:wfd-tree(A). ((w = w-nil() ∈ wfd-tree(A)) ∨ ((¬↑co-w-null(w)) ∧ (w = mk-wfd-tree(wfd-subtrees(w)) ∈ wfd-tree(A))))
BY
{ (Auto THEN (Decide ⌜↑co-w-null(w)⌝⋅ THENA Auto)) }

1
1. [A] : Type
2. w : wfd-tree(A)
3. ↑co-w-null(w)
⊢ (w = w-nil() ∈ wfd-tree(A)) ∨ ((¬↑co-w-null(w)) ∧ (w = mk-wfd-tree(wfd-subtrees(w)) ∈ wfd-tree(A)))

2
1. [A] : Type
2. w : wfd-tree(A)
3. ¬↑co-w-null(w)
⊢ (w = w-nil() ∈ wfd-tree(A)) ∨ ((¬↑co-w-null(w)) ∧ (w = mk-wfd-tree(wfd-subtrees(w)) ∈ wfd-tree(A)))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}w:wfd-tree(A).  ((w  =  w-nil())  \mvee{}  ((\mneg{}\muparrow{}co-w-null(w))  \mwedge{}  (w  =  mk-wfd-tree(wfd-subtrees(w)))))


By

---

Latex:
(Auto  THEN  (Decide  \mkleeneopen{}\muparrow{}co-w-null(w)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index