---

Step * of Lemma eqof_equal_btrue

∀[A:Type]. ∀[d:EqDecider(A)]. ∀[i,j:A].  eqof(d) i j ~ tt supposing i = j ∈ A
BY
{ (((Auto THEN (D (-4)) THEN (InstHyp [⌜i⌝; ⌜j⌝] (-4))⋅) THENA Auto)
   THEN Unfold `eqof` 0
   THEN Reduce 0
   THEN BLemma `eqtt_to_assert`
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(((Auto  THEN  (D  (-4))  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{};  \mkleeneopen{}j\mkleeneclose{}]  (-4))\mcdot{})  THENA  Auto)
  THEN  Unfold  `eqof`  0
  THEN  Reduce  0
  THEN  BLemma  `eqtt\_to\_assert`
  THEN  Auto)

---

Home Index