---

Step * 1 1 of Lemma assert_of_eq_atom2


1. x : Atom2
2. y : Atom2
3. ↑x =a2 y
4. ¬(x = y ∈ Atom2)
⊢ x = y ∈ Atom2
BY
{ (Subst ⌜x =a2 y ~ ff⌝ (-2)⋅ THEN Reduce (-2) THEN Try (Trivial)) }

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

---

Latex:

---

Latex:

1.  x  :  Atom2
2.  y  :  Atom2
3.  \muparrow{}x  =a2  y
4.  \mneg{}(x  =  y)
\mvdash{}  x  =  y


By

---

Latex:
(Subst  \mkleeneopen{}x  =a2  y  \msim{}  ff\mkleeneclose{}  (-2)\mcdot{}  THEN  Reduce  (-2)  THEN  Try  (Trivial))

---

Home Index