Step
*
of Lemma
eq_atom_wf2
∀[x,y:Atom2].  (x =a2 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:Atom2].    (x  =a2  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