---

Step * of Lemma free-dl-0-not-1

∀T:Type. ∀eq:EqDecider(T).  (¬(0 = 1 ∈ Point(free-dist-lattice(T; eq))))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (RWO "free-dl-point" (-1) THENA Auto)
   THEN (EqTypeHD (-1) THENA Auto)
   THEN Thin (-1)
   THEN RepUR ``free-dist-lattice lattice-0 lattice-1 mk-bounded-distributive-lattice`` -1
   THEN RepUR ``mk-bounded-lattice`` -1) }

1
1. T : Type
2. eq : EqDecider(T)
3. {} = {{}} ∈ fset(fset(T))
⊢ False

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).    (\mneg{}(0  =  1))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "free-dl-point"  (-1)  THENA  Auto)
  THEN  (EqTypeHD  (-1)  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RepUR  ``free-dist-lattice  lattice-0  lattice-1  mk-bounded-distributive-lattice``  -1
  THEN  RepUR  ``mk-bounded-lattice``  -1)

---

Home Index