---

Step * of Lemma eq_atom-reflexive

∀[x:Atom]. x =a x = tt
BY
{ (Auto THEN RWO "eqtt_to_assert" 0 THEN Auto THEN RWO "assert_of_eq_atom" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:Atom].  x  =a  x  =  tt


By

---

Latex:
(Auto  THEN  RWO  "eqtt\_to\_assert"  0  THEN  Auto  THEN  RWO  "assert\_of\_eq\_atom"  0  THEN  Auto)

---

Home Index