---

Step * 1 2 1 of Lemma assert-eq_var


1. a6 : Atom
2. a7 : ℕ
3. a4 : Atom
4. a5 : ℕ
5. a6 = a4 ∈ Atom
6. a7 = a5 ∈ ℤ
⊢ <a4, a5> ∈ varname()
BY
{ (Unfold `varname` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a6  :  Atom
2.  a7  :  \mBbbN{}
3.  a4  :  Atom
4.  a5  :  \mBbbN{}
5.  a6  =  a4
6.  a7  =  a5
\mvdash{}  <a4,  a5>  \mmember{}  varname()


By

---

Latex:
(Unfold  `varname`  0  THEN  Auto)

---

Home Index