---

Step * of Lemma dp-sep_wf

No Annotations
∀[d:DualPlanePrimitives]. ∀[x,y:Vec].  ((x # y) ∈ ℙ)
BY
{ (Auto THEN (Assert d ∈ DualPlanePrimitives BY Trivial) THEN (D 1 THENA Auto) THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[d:DualPlanePrimitives].  \mforall{}[x,y:Vec].    ((x  \#  y)  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto  THEN  (Assert  d  \mmember{}  DualPlanePrimitives  BY  Trivial)  THEN  (D  1  THENA  Auto)  THEN  ProveWfLemma)

---

Home Index