---

Step * of Lemma bool_ind

∀[P:𝔹 ⟶ ℙ]. (P[ff] ⇒ P[tt] ⇒ {∀b:𝔹. P[b]})
BY
{ ((Unfold `guard` 0 THEN UnivCD) THENA Auto) }

1
1. [P] : 𝔹 ⟶ ℙ
2. P[ff]
3. P[tt]
4. b : 𝔹
⊢ P[b]

---

Latex:

---

Latex:
\mforall{}[P:\mBbbB{}  {}\mrightarrow{}  \mBbbP{}].  (P[ff]  {}\mRightarrow{}  P[tt]  {}\mRightarrow{}  \{\mforall{}b:\mBbbB{}.  P[b]\})


By

---

Latex:
((Unfold  `guard`  0  THEN  UnivCD)  THENA  Auto)

---

Home Index