---

Step * of Lemma mk-dp-prim_wf

∀[V:Type]. ∀[S,P:V ⟶ V ⟶ ℙ].  ((vec=V, sep=S, perp=P) ∈ DualPlanePrimitives)
BY
{ (Auto
   THEN RepUR ``mk-dp-prim dual-plane-primitives dp-vec`` 0
   THEN RepeatFor 3 ((RecordPlusTypeCD THEN Reduce 0 THEN Try (Trivial)))
   THEN RepUR ``record record-update`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[V:Type].  \mforall{}[S,P:V  {}\mrightarrow{}  V  {}\mrightarrow{}  \mBbbP{}].    ((vec=V,  sep=S,  perp=P)  \mmember{}  DualPlanePrimitives)


By

---

Latex:
(Auto
  THEN  RepUR  ``mk-dp-prim  dual-plane-primitives  dp-vec``  0
  THEN  RepeatFor  3  ((RecordPlusTypeCD  THEN  Reduce  0  THEN  Try  (Trivial)))
  THEN  RepUR  ``record  record-update``  0
  THEN  Auto)

---

Home Index