---

Step * 1 1 of Lemma int-eq-in-rationals


1. x : ℤ
2. y : ℤ
3. ↑qeq(x;y)
⊢ x = y ∈ ℤ
BY
{ (RepUR ``qeq`` (-1)
   THEN RepeatFor 2 ((CallByValueReduce (-1) THENA Auto))
   THEN (Reduce (-1) THENA Auto)
   THEN RW assert_pushdownC (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  \muparrow{}qeq(x;y)
\mvdash{}  x  =  y


By

---

Latex:
(RepUR  ``qeq``  (-1)
  THEN  RepeatFor  2  ((CallByValueReduce  (-1)  THENA  Auto))
  THEN  (Reduce  (-1)  THENA  Auto)
  THEN  RW  assert\_pushdownC  (-1)
  THEN  Auto)

---

Home Index