---

Step * 1 of Lemma assert_of_eq_atom2


1. x : Atom2
2. y : Atom2
3. ↑x =a2 y
⊢ x = y ∈ Atom2
BY
{ Decide ⌜x = y ∈ Atom2⌝ THEN Auto⋅ }

1
1. x : Atom2
2. y : Atom2
3. ↑x =a2 y
4. ¬(x = y ∈ Atom2)
⊢ x = y ∈ Atom2

---

Latex:

---

Latex:

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


By

---

Latex:
Decide  \mkleeneopen{}x  =  y\mkleeneclose{}  THEN  Auto\mcdot{}

---

Home Index