---

Step * of Lemma free-dist-lattice-with-constraints_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))].
  (free-dist-lattice-with-constraints(T;eq;x.Cs[x]) ∈ BoundedDistributiveLattice)
BY
{ (ProveWfLemma THEN All Reduce THEN Try (FLemma `fset-contains-none-closed-downward` [-1;-2]) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[Cs:T  {}\mrightarrow{}  fset(fset(T))].
    (free-dist-lattice-with-constraints(T;eq;x.Cs[x])  \mmember{}  BoundedDistributiveLattice)


By

---

Latex:
(ProveWfLemma
  THEN  All  Reduce
  THEN  Try  (FLemma  `fset-contains-none-closed-downward`  [-1;-2])
  THEN  Auto)

---

Home Index