---

Step * of Lemma assert-eq_var

No Annotations
∀a,b:varname().  uiff(↑eq_var(a;b);a = b ∈ varname())
BY
{ Auto }

1
1. a : varname()
2. b : varname()
3. ↑eq_var(a;b)
⊢ a = b ∈ varname()

2
1. a : varname()
2. b : varname()
3. a = b ∈ varname()
⊢ ↑eq_var(a;b)

---

Latex:

---

Latex:
No  Annotations
\mforall{}a,b:varname().    uiff(\muparrow{}eq\_var(a;b);a  =  b)


By

---

Latex:
Auto

---

Home Index