---

Step * 1 of Lemma assert-eq_var


1. a : varname()
2. b : varname()
3. ↑eq_var(a;b)
⊢ a = b ∈ varname()
BY
{ (D 1
   THEN D 2
   THEN Reduce 0
   THEN Try (DProdsAndUnions)
   THEN RepUR ``eq_var`` -1
   THEN (Trivial ORELSE (RW assert_pushdownC (-1) THENA Auto))) }

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

2
1. a6 : Atom
2. a7 : ℕ
3. a4 : Atom
4. a5 : ℕ
5. (a6 = a4 ∈ Atom) ∧ (a7 = a5 ∈ ℤ)
⊢ <a6, a7> = <a4, a5> ∈ varname()

---

Latex:

---

Latex:

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


By

---

Latex:
(D  1
  THEN  D  2
  THEN  Reduce  0
  THEN  Try  (DProdsAndUnions)
  THEN  RepUR  ``eq\_var``  -1
  THEN  (Trivial  ORELSE  (RW  assert\_pushdownC  (-1)  THENA  Auto)))

---

Home Index