---

Step * of Lemma fdl-is-1_wf

∀[X:Type]. ∀[x:Point(free-dl(X))].  (fdl-is-1(x) ∈ 𝔹)
BY
{ ((Intros THEN (InstLemma `dlattice-eq-equiv` [⌜X⌝]⋅ THENA Auto))
   THEN Unhide
   THEN (Subst' Point(free-dl(X)) ~ free-dl-type(X) -2 THENA Computation)
   THEN (newQuotientElim  (-2) THENA Auto)) }

1
1. X : Type
2. X List List ∈ Type
3. ∀as,bs:X List List.  (dlattice-eq(X;as;bs) ∈ Type)
4. ∀as:X List List. dlattice-eq(X;as;as)
5. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
6. as : X List List
7. bs : X List List
8. dlattice-eq(X;as;bs)
9. 𝔹 = 𝔹 ∈ Type
⊢ fdl-is-1(as) = fdl-is-1(bs)

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[x:Point(free-dl(X))].    (fdl-is-1(x)  \mmember{}  \mBbbB{})


By

---

Latex:
((Intros  THEN  (InstLemma  `dlattice-eq-equiv`  [\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  Unhide
  THEN  (Subst'  Point(free-dl(X))  \msim{}  free-dl-type(X)  -2  THENA  Computation)
  THEN  (newQuotientElim    (-2)  THENA  Auto))

---

Home Index