---

Step * of Lemma free-dl-basis

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(free-dist-lattice(T; eq))].
  (x = \/(λs./\(λx.free-dl-inc(x)"(s))"(x)) ∈ Point(free-dist-lattice(T; eq)))
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-dist-lattice(T; eq))
⊢ x = \/(λs./\(λx.free-dl-inc(x)"(s))"(x)) ∈ Point(free-dist-lattice(T; eq))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:Point(free-dist-lattice(T;  eq))].
    (x  =  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(s))"(x)))


By

---

Latex:
Auto

---

Home Index