---

Step * 1 of Lemma evodd-induction2


1. [Q] : b:𝔹 ⟶ (pw-evenodd() b) ⟶ ℙ
2. Q[tt;evodd-zero()]
3. ∀b:𝔹. ∀x:pw-evenodd() b.  (Q[b;x] ⇒ Q[¬bb;evodd-succ(x)])
4. b : 𝔹
5. x : b = tt
6. f : Void ⟶ (pw-evenodd() (¬bb))
7. ∀x:Void. Q[¬bb;f x]
⊢ Q[b;pW-sup(inl Ax;f)]
BY
{ (HypSubst' (-3) 0 THEN NthHypEq 2 THEN EqCD THEN Auto) }

1
.....subterm..... T:t
2:n
1. Q : b:𝔹 ⟶ (pw-evenodd() b) ⟶ ℙ
2. Q[tt;evodd-zero()]
3. ∀b:𝔹. ∀x:pw-evenodd() b.  (Q[b;x] ⇒ Q[¬bb;evodd-succ(x)])
4. b : 𝔹
5. x : b = tt
6. f : Void ⟶ (pw-evenodd() (¬bb))
7. ∀x:Void. Q[¬bb;f x]
⊢ pW-sup(inl Ax;f) = evodd-zero() ∈ (pw-evenodd() tt)

---

Latex:

---

Latex:

1.  [Q]  :  b:\mBbbB{}  {}\mrightarrow{}  (pw-evenodd()  b)  {}\mrightarrow{}  \mBbbP{}
2.  Q[tt;evodd-zero()]
3.  \mforall{}b:\mBbbB{}.  \mforall{}x:pw-evenodd()  b.    (Q[b;x]  {}\mRightarrow{}  Q[\mneg{}\msubb{}b;evodd-succ(x)])
4.  b  :  \mBbbB{}
5.  x  :  b  =  tt
6.  f  :  Void  {}\mrightarrow{}  (pw-evenodd()  (\mneg{}\msubb{}b))
7.  \mforall{}x:Void.  Q[\mneg{}\msubb{}b;f  x]
\mvdash{}  Q[b;pW-sup(inl  Ax;f)]


By

---

Latex:
(HypSubst'  (-3)  0  THEN  NthHypEq  2  THEN  EqCD  THEN  Auto)

---

Home Index