---

Step * of Lemma free-dma-lift-0

∀T:Type. ∀eq:EqDecider(T). ∀dm:DeMorganAlgebra. ∀eq2:EqDecider(Point(dm)). ∀f:T ⟶ Point(dm).
∀x:Point(free-DeMorgan-algebra(T;eq)).
  (free-dma-lift(T;eq;dm;eq2;f) x) = 0 ∈ Point(dm) supposing x = 0 ∈ Point(free-DeMorgan-algebra(T;eq))
BY
{ (Auto THEN (HypSubst' -1 0 THENA Auto) THEN GenConclAtAddr [2;1] THEN RepeatFor 3 (DVar `v') THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}dm:DeMorganAlgebra.  \mforall{}eq2:EqDecider(Point(dm)).  \mforall{}f:T  {}\mrightarrow{}  Point(dm).
\mforall{}x:Point(free-DeMorgan-algebra(T;eq)).
    (free-dma-lift(T;eq;dm;eq2;f)  x)  =  0  supposing  x  =  0


By

---

Latex:
(Auto
  THEN  (HypSubst'  -1  0  THENA  Auto)
  THEN  GenConclAtAddr  [2;1]
  THEN  RepeatFor  3  (DVar  `v')
  THEN  Auto)

---

Home Index