---

Step * of Lemma comparison-reflexive

∀[T:Type]. ∀cmp:comparison(T). ∀x:T.  ((cmp x x) = 0 ∈ ℤ)
BY
{ (Auto THEN D 2 THEN Auto THEN InstHyp [⌜x⌝;⌜x⌝] 3⋅ THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}cmp:comparison(T).  \mforall{}x:T.    ((cmp  x  x)  =  0)


By

---

Latex:
(Auto  THEN  D  2  THEN  Auto  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  3\mcdot{}  THEN  Auto')

---

Home Index