---

Step * 1 2 of Lemma assert-eq_var


1. a6 : Atom
2. a7 : ℕ
3. a4 : Atom
4. a5 : ℕ
5. (a6 = a4 ∈ Atom) ∧ (a7 = a5 ∈ ℤ)
⊢ <a6, a7> = <a4, a5> ∈ varname()
BY
{ (D -1 THEN (HypSubst' (-1) 0 THEN HypSubst' (-2) 0) THEN Fold `member` 0) }

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index