---

Step * 1 of Lemma atom_dset_wf


IsEqFun(Atom;λx,y. x =a y)
BY
{ AbEval ``eqfun_p`` 0 
THEN ((RW bool_to_propC 0) THEN Auto) 
 }

---

Latex:

---

Latex:

IsEqFun(Atom;\mlambda{}x,y.  x  =a  y)


By

---

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

---

Home Index