Step * 1 of Lemma sq_stable__free-from-atom2


1. Type
2. T
3. Atom2
4. a#x:T
⊢ Ax ∈ a#x:T
BY
(Unfold `member` THEN Refine_freeFromAtomAxiom THEN Auto) }


Latex:


Latex:

1.  T  :  Type
2.  x  :  T
3.  a  :  Atom2
4.  a\#x:T
\mvdash{}  Ax  \mmember{}  a\#x:T


By


Latex:
(Unfold  `member`  0  THEN  Refine\_freeFromAtomAxiom  THEN  Auto)




Home Index