---

Step * 2 1 of Lemma assert_of_eq_atom1

.....equality..... 
1. x : Atom1
2. y : Atom1
3. x = y ∈ Atom1
⊢ x =a1 y ~ tt
BY
{ (Unfold `eq_atom` 0 THEN Refine_atomn_eqReduceTrueSq THEN Auto)⋅ }

---

Latex:

---

Latex:
.....equality..... 
1.  x  :  Atom1
2.  y  :  Atom1
3.  x  =  y
\mvdash{}  x  =a1  y  \msim{}  tt


By

---

Latex:
(Unfold  `eq\_atom`  0  THEN  Refine\_atomn\_eqReduceTrueSq  THEN  Auto)\mcdot{}

---

Home Index