---

Step * of Lemma fun-ss_wf

∀[ss:SeparationSpace]. ∀[A:Type].  (A ⟶ ss ∈ SeparationSpace)
BY
{ (ProveWfLemma
   THEN Try (((MemTypeCD THEN Auto)
              THEN Reduce 0
              THEN (D 0 THENA Auto)
              THEN D -1
              THEN MoveToConcl (-1)
              THEN Fold `not` 0
              THEN Auto))
   THEN (Assert ss ∈ SeparationSpace BY
               Auto)
   THEN (D 1 THENA Auto)
   THEN All (Folds ``ss-point ss-sep``) 
   THEN All (Unfolds  ``all implies``)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[ss:SeparationSpace].  \mforall{}[A:Type].    (A  {}\mrightarrow{}  ss  \mmember{}  SeparationSpace)


By

---

Latex:
(ProveWfLemma
  THEN  Try  (((MemTypeCD  THEN  Auto)
                        THEN  Reduce  0
                        THEN  (D  0  THENA  Auto)
                        THEN  D  -1
                        THEN  MoveToConcl  (-1)
                        THEN  Fold  `not`  0
                        THEN  Auto))
  THEN  (Assert  ss  \mmember{}  SeparationSpace  BY
                          Auto)
  THEN  (D  1  THENA  Auto)
  THEN  All  (Folds  ``ss-point  ss-sep``) 
  THEN  All  (Unfolds    ``all  implies``)\mcdot{}
  THEN  Auto)

---

Home Index