---

Step * 1 of Lemma evodd-enum-surjection


∀b1:𝔹. ∀b2:pw-evenodd() b1.  ∃a:ℕ. (evodd-enum(a) = <b1, b2> ∈ (b:𝔹 × (pw-evenodd() b)))
BY
{ (InstLemma `evodd-induction2-ext` [⌜λ2b1 b2.∃a:ℕ. (evodd-enum(a) = <b1, b2> ∈ (b:𝔹 × (pw-evenodd() b)))⌝]⋅
   THEN Auto
   ) }

1
.....antecedent..... 
∃a:ℕ. (evodd-enum(a) = <tt, evodd-zero()> ∈ (b:𝔹 × (pw-evenodd() b)))

2
1. b : 𝔹
2. x : pw-evenodd() b
3. ∃a:ℕ. (evodd-enum(a) = <b, x> ∈ (b:𝔹 × (pw-evenodd() b)))
⊢ ∃a:ℕ. (evodd-enum(a) = <¬bb, evodd-succ(x)> ∈ (b:𝔹 × (pw-evenodd() b)))

---

Latex:

---

Latex:

\mforall{}b1:\mBbbB{}.  \mforall{}b2:pw-evenodd()  b1.    \mexists{}a:\mBbbN{}.  (evodd-enum(a)  =  <b1,  b2>)


By

---

Latex:
(InstLemma  `evodd-induction2-ext`  [\mkleeneopen{}\mlambda{}\msubtwo{}b1  b2.\mexists{}a:\mBbbN{}.  (evodd-enum(a)  =  <b1,  b2>)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index