---

Step * 1 of Lemma assert_of_eq_atom1


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

1
1. x : Atom1
2. y : Atom1
3. ↑x =a1 y
4. ¬(x = y ∈ Atom1)
⊢ x = y ∈ Atom1

---

Latex:

---

Latex:

1.  x  :  Atom1
2.  y  :  Atom1
3.  \muparrow{}x  =a1  y
\mvdash{}  x  =  y


By

---

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

---

Home Index