---

Step * of Lemma decdr-to-bool_wf

∀[T:Type]. ∀[A,B:T ⟶ ℙ]. ∀[d:x:T ⟶ (A[x] + B[x])].  (bool(d) ∈ T ⟶ 𝔹)
BY
{ (Intros THEN Unhide) }

1
1. T : Type
2. A : T ⟶ ℙ
3. B : T ⟶ ℙ
4. d : x:T ⟶ (A[x] + B[x])
⊢ bool(d) ∈ T ⟶ 𝔹

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[A,B:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:x:T  {}\mrightarrow{}  (A[x]  +  B[x])].    (bool(d)  \mmember{}  T  {}\mrightarrow{}  \mBbbB{})


By

---

Latex:
(Intros  THEN  Unhide)

---

Home Index