---

Step * of Lemma mk-pgeo-prim_wf

∀[P,L:Type]. ∀[S:P ⟶ L ⟶ ℙ].  (points=P lines=L plsep=S ∈ ProjGeomPrimitives)
BY
{ (Auto
   THEN RepUR ``mk-pgeo-prim pgeo-primitives pgeo-point pgeo-line`` 0
   THEN RepeatFor 3 ((RecordPlusTypeCD THEN Reduce 0 THEN Try (Trivial)))
   THEN RepUR ``record record-update`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P,L:Type].  \mforall{}[S:P  {}\mrightarrow{}  L  {}\mrightarrow{}  \mBbbP{}].    (points=P  lines=L  plsep=S  \mmember{}  ProjGeomPrimitives)


By

---

Latex:
(Auto
  THEN  RepUR  ``mk-pgeo-prim  pgeo-primitives  pgeo-point  pgeo-line``  0
  THEN  RepeatFor  3  ((RecordPlusTypeCD  THEN  Reduce  0  THEN  Try  (Trivial)))
  THEN  RepUR  ``record  record-update``  0
  THEN  Auto)

---

Home Index