---

Step * of Lemma face-lattice0_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T].  ((x=0) ∈ Point(face-lattice(T;eq)))
BY
{ (Auto
   THEN (InstLemma `free-dlwc-inc_wf` [⌜T + T⌝;⌜union-deq(T;T;eq;eq)⌝;⌜λ2x.face-lattice-constraints(x)⌝;⌜inl x⌝]⋅
         THENA Auto
         )
   THEN Fold `face-lattice` (-1)
   THEN (NthHypSq (-1) THEN EqCD)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].    ((x=0)  \mmember{}  Point(face-lattice(T;eq)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `free-dlwc-inc\_wf`  [\mkleeneopen{}T  +  T\mkleeneclose{};\mkleeneopen{}union-deq(T;T;eq;eq)\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}x.face-lattice-constraints(x)\mkleeneclose{};\mkleeneopen{}inl  x\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Fold  `face-lattice`  (-1)
  THEN  (NthHypSq  (-1)  THEN  EqCD)
  THEN  Auto)

---

Home Index