---

Step * 1 1 1 of Lemma assert-eq_var


1. a2 : Atom
2. a3 : Atom
3. a2 = a3 ∈ Atom
⊢ a3 ∈ varname()
BY
{ (Unfold `varname` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a2  :  Atom
2.  a3  :  Atom
3.  a2  =  a3
\mvdash{}  a3  \mmember{}  varname()


By

---

Latex:
(Unfold  `varname`  0  THEN  Auto)

---

Home Index