---

Step * of Lemma fl-vertex_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[u:T + T].  (fl-vertex(u) ∈ Point(face-lattice(T;eq)))
BY
{ ((Auto THEN D -1) THEN Unfold `fl-vertex` 0 THEN Folds ``face-lattice0 face-lattice1`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[u:T  +  T].    (fl-vertex(u)  \mmember{}  Point(face-lattice(T;eq)))


By

---

Latex:
((Auto  THEN  D  -1)  THEN  Unfold  `fl-vertex`  0  THEN  Folds  ``face-lattice0  face-lattice1``  0  THEN  Auto)

---

Home Index