---

Step * 2 1 of Lemma assert_of_eq_atom2

.....equality..... 
1. x : Atom2
2. y : Atom2
3. x = y ∈ Atom2
⊢ x =a2 y ~ tt
BY
{ (Unfold `eq_atom` 0 THEN Refine `atomn_eqReduceTrueSq` [] THEN Auto)⋅ }

---

Latex:

---

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


By

---

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

---

Home Index