---

Step * 1 1 of Lemma assert-is-dml-1


1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-DeMorgan-lattice(T;eq))
4. v : EqDecider(Point(free-DeMorgan-lattice(T;eq)))
5. free-dml-deq(T;eq) = v ∈ EqDecider(Point(free-DeMorgan-lattice(T;eq)))
⊢ uiff(↑(v x 1);x = 1 ∈ Point(free-DeMorgan-lattice(T;eq)))
BY
{ (DVar `v' THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  Point(free-DeMorgan-lattice(T;eq))
4.  v  :  EqDecider(Point(free-DeMorgan-lattice(T;eq)))
5.  free-dml-deq(T;eq)  =  v
\mvdash{}  uiff(\muparrow{}(v  x  1);x  =  1)


By

---

Latex:
(DVar  `v'  THEN  Auto)

---

Home Index