---

Step * of Lemma evodd-succ_wf

∀[b:𝔹]. ∀[n:pw-evenodd() (¬bb)].  (evodd-succ(n) ∈ pw-evenodd() b)
BY
{ TACTIC:(Unfold `pw-evenodd` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[b:\mBbbB{}].  \mforall{}[n:pw-evenodd()  (\mneg{}\msubb{}b)].    (evodd-succ(n)  \mmember{}  pw-evenodd()  b)


By

---

Latex:
TACTIC:(Unfold  `pw-evenodd`  0  THEN  ProveWfLemma)

---

Home Index