---

Step * 1 1 of Lemma assert_of_eq_atom1


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index