---

Step * 1 1 of Lemma fdl-eq-1


1. X : Type
2. x : as,bs:X List List//dlattice-eq(X;as;bs)
⊢ fdl-is-1(x) ∈ 𝔹
BY
{ ((Fold `free-dl-type` (-1) THEN Auto)
   THEN (Subst' free-dl-type(X) ~ Point(free-dl(X)) -1 THENA Computation)
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  x  :  as,bs:X  List  List//dlattice-eq(X;as;bs)
\mvdash{}  fdl-is-1(x)  \mmember{}  \mBbbB{}


By

---

Latex:
((Fold  `free-dl-type`  (-1)  THEN  Auto)
  THEN  (Subst'  free-dl-type(X)  \msim{}  Point(free-dl(X))  -1  THENA  Computation)
  THEN  Auto)

---

Home Index