---

Step * 1 1 1 of Lemma assert_of_eq_atom1

.....equality..... 
1. x : Atom1
2. y : Atom1
3. ↑x =a1 y
4. ¬(x = y ∈ Atom1)
⊢ x =a1 y ~ ff
BY
{ (OnConcl (Unfold_o Obid: eq_atomn)  THEN Refine_atomn_eqReduceFalseSq THEN Auto)⋅ }

---

Latex:

---

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


By

---

Latex:
(OnConcl  (Unfold\_o  Obid:  eq\_atomn)    THEN  Refine\_atomn\_eqReduceFalseSq  THEN  Auto)\mcdot{}

---

Home Index