---

Step * of Lemma eq_atom_wf1

∀[x,y:Atom1].  (x =a1 y ∈ 𝔹)
BY
{ Auto
THEN Try (Unfold `member` 0
          THEN Refine_atomnEquality)
THEN Unfold `eq_atom` 0
THEN Unfold `member` 0
THEN Refine_atomn_eqEquality `v'
THEN Auto⋅ }

---

Latex:

---

Latex:
\mforall{}[x,y:Atom1].    (x  =a1  y  \mmember{}  \mBbbB{})


By

---

Latex:
Auto
THEN  Try  (Unfold  `member`  0
                    THEN  Refine\_atomnEquality)
THEN  Unfold  `eq\_atom`  0
THEN  Unfold  `member`  0
THEN  Refine\_atomn\_eqEquality  `v'
THEN  Auto\mcdot{}

---

Home Index