---

Step * 1 of Lemma decdr-to-bool_wf


1. T : Type
2. A : T ⟶ ℙ
3. B : T ⟶ ℙ
4. d : x:T ⟶ (A[x] + B[x])
⊢ bool(d) ∈ T ⟶ 𝔹
BY
{ (Unfold `decdr-to-bool` 0 THEN Fold `it` 0 THEN Folds ``btrue bfalse`` 0 THEN RepUR ``ifthenelse`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  T  {}\mrightarrow{}  \mBbbP{}
3.  B  :  T  {}\mrightarrow{}  \mBbbP{}
4.  d  :  x:T  {}\mrightarrow{}  (A[x]  +  B[x])
\mvdash{}  bool(d)  \mmember{}  T  {}\mrightarrow{}  \mBbbB{}


By

---

Latex:
(Unfold  `decdr-to-bool`  0
  THEN  Fold  `it`  0
  THEN  Folds  ``btrue  bfalse``  0
  THEN  RepUR  ``ifthenelse``  0
  THEN  Auto)

---

Home Index