---

Step * of Lemma mk_deq_wf

∀[T:Type]. ∀[p:∀x,y:T.  Dec(x = y ∈ T)].  (mk_deq(p) ∈ EqDecider(T))
BY
{ (Auto THEN Unfolds ``mk_deq deq`` 0) }

1
1. T : Type
2. p : ∀x,y:T.  Dec(x = y ∈ T)
⊢ λx,y. isl(p x y) ∈ {eq:T ⟶ T ⟶ 𝔹| ∀x,y:T.  (x = y ∈ T ⇐⇒ ↑(eq x y))} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[p:\mforall{}x,y:T.    Dec(x  =  y)].    (mk\_deq(p)  \mmember{}  EqDecider(T))


By

---

Latex:
(Auto  THEN  Unfolds  ``mk\_deq  deq``  0)

---

Home Index