---

Step * 1 1 of Lemma assert-eq_var


1. a2 : Atom
2. a3 : Atom
3. a2 = a3 ∈ Atom
⊢ a2 = a3 ∈ varname()
BY
{ (HypSubst' (-1) 0 THEN Fold `member` 0) }

1
1. a2 : Atom
2. a3 : Atom
3. a2 = a3 ∈ Atom
⊢ a3 ∈ varname()

---

Latex:

---

Latex:

1.  a2  :  Atom
2.  a3  :  Atom
3.  a2  =  a3
\mvdash{}  a2  =  a3


By

---

Latex:
(HypSubst'  (-1)  0  THEN  Fold  `member`  0)

---

Home Index