---

Step * 1 of Lemma bool_ind


1. [P] : 𝔹 ⟶ ℙ
2. P[ff]
3. P[tt]
4. b : 𝔹
⊢ P[b]
BY
{ (BoolInd 4 THEN Auto) }

---

Latex:

---

Latex:

1.  [P]  :  \mBbbB{}  {}\mrightarrow{}  \mBbbP{}
2.  P[ff]
3.  P[tt]
4.  b  :  \mBbbB{}
\mvdash{}  P[b]


By

---

Latex:
(BoolInd  4  THEN  Auto)

---

Home Index