---

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


1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-DeMorgan-lattice(T;eq))
⊢ uiff(↑is-dml-1(T;eq;x);x = 1 ∈ Point(free-DeMorgan-lattice(T;eq)))
BY
{ (Unfold `is-dml-1` 0 THEN (GenConclTerm ⌜free-dml-deq(T;eq)⌝⋅ THENA Auto)) }

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)))

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `is-dml-1`  0  THEN  (GenConclTerm  \mkleeneopen{}free-dml-deq(T;eq)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index