---

Step * of Lemma name_eq_symmetry

∀[x,y:Name].  (name_eq(x;y) ~ name_eq(y;x))
BY
{ (Auto THEN (BLemma `iff_imp_equal_bool` THENM RWO "assert-name_eq" 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:Name].    (name\_eq(x;y)  \msim{}  name\_eq(y;x))


By

---

Latex:
(Auto  THEN  (BLemma  `iff\_imp\_equal\_bool`  THENM  RWO  "assert-name\_eq"  0)  THEN  Auto)

---

Home Index