---

Step * of Lemma eqof_eq_btrue

∀[A:Type]. ∀[d:EqDecider(A)]. ∀[i:A].  (eqof(d) i i ~ tt)
BY
{ (((Auto THEN (D (-2)) THEN (InstHyp [⌜i⌝; ⌜i⌝] (-2))⋅) THENA Auto) THEN Unfold `eqof` 0 THEN Reduce 0) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[d:EqDecider(A)].  \mforall{}[i:A].    (eqof(d)  i  i  \msim{}  tt)


By

---

Latex:
(((Auto  THEN  (D  (-2))  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{};  \mkleeneopen{}i\mkleeneclose{}]  (-2))\mcdot{})  THENA  Auto)
  THEN  Unfold  `eqof`  0
  THEN  Reduce  0)

---

Home Index