---

Step * of Lemma deq-implies

∀[T:Type]. (EqDecider(T) ⇒ {∀x,y:T.  Dec(x = y ∈ T)})
BY
{ (Auto THEN D 0 THEN Auto THEN RenameVar `eq' 2 THEN UseWitness ⌜eq x y⌝⋅) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. y : T
⊢ eq x y ∈ Dec(x = y ∈ T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  (EqDecider(T)  {}\mRightarrow{}  \{\mforall{}x,y:T.    Dec(x  =  y)\})


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  RenameVar  `eq'  2  THEN  UseWitness  \mkleeneopen{}eq  x  y\mkleeneclose{}\mcdot{})

---

Home Index