---

Step * of Lemma w-nil_wf

∀[A:Type]. (w-nil() ∈ wfd-tree(A))
BY
{ (ProveWfLemma
   THEN (InstLemma `co-w-ext` [A]⋅ THENA Auto)
   THEN (Assert inl ⋅ ∈ co-w(A) BY
               (SubsumeC ⌜Unit + (A ⟶ co-w(A))⌝⋅ THEN Auto))
   THEN MemTypeCD
   THEN Auto) }

1
1. A : Type
2. co-w(A) ≡ Unit + (A ⟶ co-w(A))
3. inl ⋅ ∈ co-w(A)
4. p : ℕ ⟶ A@i
⊢ w-bars(inl ⋅;p)

---

Latex:

---

Latex:
\mforall{}[A:Type].  (w-nil()  \mmember{}  wfd-tree(A))


By

---

Latex:
(ProveWfLemma
  THEN  (InstLemma  `co-w-ext`  [A]\mcdot{}  THENA  Auto)
  THEN  (Assert  inl  \mcdot{}  \mmember{}  co-w(A)  BY
                          (SubsumeC  \mkleeneopen{}Unit  +  (A  {}\mrightarrow{}  co-w(A))\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index