---

Step * 2 of Lemma assert_of_eq_atom2


1. x : Atom2
2. y : Atom2
3. x = y ∈ Atom2
⊢ ↑x =a2 y
BY
{ (Subst' x =a2 y ~ tt 0 THEN Reduce 0 THEN Try (Trivial)) }

1
.....equality..... 
1. x : Atom2
2. y : Atom2
3. x = y ∈ Atom2
⊢ x =a2 y ~ tt

---

Latex:

---

Latex:

1.  x  :  Atom2
2.  y  :  Atom2
3.  x  =  y
\mvdash{}  \muparrow{}x  =a2  y


By

---

Latex:
(Subst'  x  =a2  y  \msim{}  tt  0  THEN  Reduce  0  THEN  Try  (Trivial))

---

Home Index