---

Step * 2 of Lemma assert-eq_var


1. a : varname()
2. b : varname()
3. a = b ∈ varname()
⊢ ↑eq_var(a;b)
BY
{ ((RWO "-1" 0 THENA Auto) THEN All Thin) }

1
1. b : varname()
⊢ ↑eq_var(b;b)

---

Latex:

---

Latex:

1.  a  :  varname()
2.  b  :  varname()
3.  a  =  b
\mvdash{}  \muparrow{}eq\_var(a;b)


By

---

Latex:
((RWO  "-1"  0  THENA  Auto)  THEN  All  Thin)

---

Home Index