---

Step * 1 of Lemma int_loset_wf


IsEqFun(ℤ;λx,y. (x =z y))
BY
{ Unfold `eqfun_p` 0 
THEN AbReduce 0 
THEN ((RW bool_to_propC 0) THEN Auto) }

---

Latex:

---

Latex:

IsEqFun(\mBbbZ{};\mlambda{}x,y.  (x  =\msubz{}  y))


By

---

Latex:
Unfold  `eqfun\_p`  0 
THEN  AbReduce  0 
THEN  ((RW  bool\_to\_propC  0)  THEN  Auto)

---

Home Index