---

Step * of Lemma free-dml-deq_wf

∀[T:Type]. ∀[eq:EqDecider(T)].  (free-dml-deq(T;eq) ∈ EqDecider(Point(free-DeMorgan-lattice(T;eq))))
BY
{ (Auto THEN Unfold `free-DeMorgan-lattice` 0 THEN (RWO "free-dl-point" 0 THENA Auto) THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].    (free-dml-deq(T;eq)  \mmember{}  EqDecider(Point(free-DeMorgan-lattice(T;eq))))


By

---

Latex:
(Auto
  THEN  Unfold  `free-DeMorgan-lattice`  0
  THEN  (RWO  "free-dl-point"  0  THENA  Auto)
  THEN  ProveWfLemma)

---

Home Index