---

Step * 1 1 1 of Lemma assert_of_eq_atom2

.....equality..... 
1. x : Atom2
2. y : Atom2
3. ↑x =a2 y
4. ¬(x = y ∈ Atom2)
⊢ x =a2 y ~ ff
BY
{ (Unfold `eq_atom` 0 THEN Refine `atomn_eqReduceFalseSq` [] THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `eq\_atom`  0  THEN  Refine  `atomn\_eqReduceFalseSq`  []  THEN  Auto)

---

Home Index