---

Step * 1 1 of Lemma bool-to-dcdr_wf

.....assertion..... 
1. A : Type
2. f : A ⟶ 𝔹
3. x : A
⊢ {f}b ∈ ∀x:A. Dec(f x = tt)
BY
{ (Unfold `bool-to-dcdr` 0⋅ THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  \mBbbB{}
3.  x  :  A
\mvdash{}  \{f\}\msubb{}  \mmember{}  \mforall{}x:A.  Dec(f  x  =  tt)


By

---

Latex:
(Unfold  `bool-to-dcdr`  0\mcdot{}  THEN  Auto)

---

Home Index