---

Step * of Lemma coW2natinf_wf

∀[n:ℕ]. ∀[w:coW(ℕ2;x.if (x =z 0) then Void else Unit fi )].  (coW2natinf(w;n) ∈ 𝔹)
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN NatInd (-1)
   THEN (D 0 THENA Auto)
   THEN coWD (-1)
   THEN D -1
   THEN Unfold `coW2natinf` 0
   THEN Reduce 0
   THEN RepUR ``coW-item`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[w:coW(\mBbbN{}2;x.if  (x  =\msubz{}  0)  then  Void  else  Unit  fi  )].    (coW2natinf(w;n)  \mmember{}  \mBbbB{})


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  NatInd  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  coWD  (-1)
  THEN  D  -1
  THEN  Unfold  `coW2natinf`  0
  THEN  Reduce  0
  THEN  RepUR  ``coW-item``  0
  THEN  Auto)

---

Home Index