---

Step * of Lemma dm-neg_wf

No Annotations
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(free-DeMorgan-lattice(T;eq))].  (¬(x) ∈ Point(free-DeMorgan-lattice(T;eq)))
BY
{ (Auto
   THEN Unfold `dm-neg` 0
   THEN (Assert Point(free-DeMorgan-lattice(T;eq)) ~ Point(opposite-lattice(free-DeMorgan-lattice(T;eq))) BY
               (RW (SubC (SymbCompC [`free-DeMorgan-lattice`] 30)) 0 THEN Auto))
   THEN HypSubst'  (-1) 0
   THEN MemCD
   THEN Try (QuickAuto)
   THEN RevHypSubst (-1) 0
   THEN Unfold `free-DeMorgan-lattice` 0
   THEN RWO "free-dl-point" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:Point(free-DeMorgan-lattice(T;eq))].
    (\mneg{}(x)  \mmember{}  Point(free-DeMorgan-lattice(T;eq)))


By

---

Latex:
(Auto
  THEN  Unfold  `dm-neg`  0
  THEN  (Assert  Point(free-DeMorgan-lattice(T;eq)) 
                          \msim{}  Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))  BY
                          (RW  (SubC  (SymbCompC  [`free-DeMorgan-lattice`]  30))  0  THEN  Auto))
  THEN  HypSubst'    (-1)  0
  THEN  MemCD
  THEN  Try  (QuickAuto)
  THEN  RevHypSubst  (-1)  0
  THEN  Unfold  `free-DeMorgan-lattice`  0
  THEN  RWO  "free-dl-point"  0
  THEN  Auto)

---

Home Index