---

Step * of Lemma assert_of_eq_int_rw

∀[x,y:ℤ].  {uiff(↑(x =z y);x = y ∈ ℤ)}
BY
{ (Unfold `guard` 0 THEN Lemma `assert_of_eq_int`) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbZ{}].    \{uiff(\muparrow{}(x  =\msubz{}  y);x  =  y)\}


By

---

Latex:
(Unfold  `guard`  0  THEN  Lemma  `assert\_of\_eq\_int`)

---

Home Index