---

Step * 1 of Lemma w-nil_wf


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)
BY
{ (D 0 THEN Auto THEN With ⌜0⌝ (D 0)⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  co-w(A)  \mequiv{}  Unit  +  (A  {}\mrightarrow{}  co-w(A))
3.  inl  \mcdot{}  \mmember{}  co-w(A)
4.  p  :  \mBbbN{}  {}\mrightarrow{}  A@i
\mvdash{}  w-bars(inl  \mcdot{};p)


By

---

Latex:
(D  0  THEN  Auto  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index