---

Step * of Lemma fl-all_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[phi:Point(face-lattice(T;eq))]. ∀[i:T].  ((∀i.phi) ∈ Point(face-lattice(T;eq)))
BY
{ ProveWfLemma }

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index