---

Step * of Lemma decidable__equal_int

∀x,y:ℤ.  Dec(x = y ∈ ℤ)
BY
{ (InstLemma `decidable__int_equal` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.    Dec(x  =  y)


By

---

Latex:
(InstLemma  `decidable\_\_int\_equal`  []  THEN  Trivial)

---

Home Index