---

Step * of Lemma mk-ss_wf

∀[P:Type]. ∀[Sep:{s:P ⟶ P ⟶ ℙ| ∀x:P. (¬(s x x))} ]. ∀[Sym:∀x,y:P.  ((Sep x y) ⇒ (Sep y x))]. ∀[C:∀x,y,z:P.
                                                                                                     ((Sep x y)
                                                                                                     ⇒ ((Sep x z)
                                                                                                        ∨ (Sep y z)))].
  (Point=P
   #=Sep
   symm=Sym
   cotrans=C ∈ SeparationSpace)
BY
{ (Auto
   THEN RepUR ``mk-ss separation-space`` 0
   THEN RepeatFor 4 ((RecordPlusTypeCD THENL [ Id; (Reduce 0 THEN Try (Trivial))]))
   THEN RepUR ``record record-update`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[Sep:\{s:P  {}\mrightarrow{}  P  {}\mrightarrow{}  \mBbbP{}|  \mforall{}x:P.  (\mneg{}(s  x  x))\}  ].  \mforall{}[Sym:\mforall{}x,y:P.    ((Sep  x  y)  {}\mRightarrow{}  (Sep  y  x))].
\mforall{}[C:\mforall{}x,y,z:P.    ((Sep  x  y)  {}\mRightarrow{}  ((Sep  x  z)  \mvee{}  (Sep  y  z)))].
    (Point=P
      \#=Sep
      symm=Sym
      cotrans=C  \mmember{}  SeparationSpace)


By

---

Latex:
(Auto
  THEN  RepUR  ``mk-ss  separation-space``  0
  THEN  RepeatFor  4  ((RecordPlusTypeCD  THENL  [  Id;  (Reduce  0  THEN  Try  (Trivial))]))
  THEN  RepUR  ``record  record-update``  0
  THEN  Auto)

---

Home Index