---

Step * 1 of Lemma free-dl-generators


1. X : Type
2. free-dl-type(X) ~ free-dl-type(X)
3. free-dl-type(X) = free-dl-type(X) ∈ Type
4. L : BoundedDistributiveLattice
5. f : free-dl-type(X) ⟶ Point(L)
6. ∀[a,b:free-dl-type(X)].  ((f a ∧ f b = (f a ∧ b) ∈ Point(L)) ∧ (f a ∨ f b = (f a ∨ b) ∈ Point(L)))
7. (f 0) = 0 ∈ Point(L)
8. (f 1) = 1 ∈ Point(L)
9. g : free-dl-type(X) ⟶ Point(L)
10. ∀[a,b:free-dl-type(X)].  ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
11. (g 0) = 0 ∈ Point(L)
12. (g 1) = 1 ∈ Point(L)
13. ∀x:X. ((f free-dl-generator(x)) = (g free-dl-generator(x)) ∈ Point(L))
14. x : free-dl-type(X)
⊢ (f x) = (g x) ∈ Point(L)
BY
{ ((InstLemma `dlattice-eq-equiv` [⌜X⌝]⋅ THEN Auto)
   THEN (newQuotientElim (-2) ⋅ THENA Auto)
   THEN (Subst' bs = as ∈ free-dl-type(X) 0 THENA (Try (EqTypeCD) THEN Auto))
   THEN ThinVar `bs'
   THEN Thin (-1)) }

1
1. X : Type
2. free-dl-type(X) ~ free-dl-type(X)
3. free-dl-type(X) = free-dl-type(X) ∈ Type
4. L : BoundedDistributiveLattice
5. f : free-dl-type(X) ⟶ Point(L)
6. ∀[a,b:free-dl-type(X)].  ((f a ∧ f b = (f a ∧ b) ∈ Point(L)) ∧ (f a ∨ f b = (f a ∨ b) ∈ Point(L)))
7. (f 0) = 0 ∈ Point(L)
8. (f 1) = 1 ∈ Point(L)
9. g : free-dl-type(X) ⟶ Point(L)
10. ∀[a,b:free-dl-type(X)].  ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
11. (g 0) = 0 ∈ Point(L)
12. (g 1) = 1 ∈ Point(L)
13. ∀x:X. ((f free-dl-generator(x)) = (g free-dl-generator(x)) ∈ Point(L))
14. X List List ∈ Type
15. ∀as,bs:X List List.  (dlattice-eq(X;as;bs) ∈ Type)
16. ∀as:X List List. dlattice-eq(X;as;as)
17. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
18. as : X List List
⊢ (f as) = (g as) ∈ Point(L)

---

Latex:

---

Latex:

1.  X  :  Type
2.  free-dl-type(X)  \msim{}  free-dl-type(X)
3.  free-dl-type(X)  =  free-dl-type(X)
4.  L  :  BoundedDistributiveLattice
5.  f  :  free-dl-type(X)  {}\mrightarrow{}  Point(L)
6.  \mforall{}[a,b:free-dl-type(X)].    ((f  a  \mwedge{}  f  b  =  (f  a  \mwedge{}  b))  \mwedge{}  (f  a  \mvee{}  f  b  =  (f  a  \mvee{}  b)))
7.  (f  0)  =  0
8.  (f  1)  =  1
9.  g  :  free-dl-type(X)  {}\mrightarrow{}  Point(L)
10.  \mforall{}[a,b:free-dl-type(X)].    ((g  a  \mwedge{}  g  b  =  (g  a  \mwedge{}  b))  \mwedge{}  (g  a  \mvee{}  g  b  =  (g  a  \mvee{}  b)))
11.  (g  0)  =  0
12.  (g  1)  =  1
13.  \mforall{}x:X.  ((f  free-dl-generator(x))  =  (g  free-dl-generator(x)))
14.  x  :  free-dl-type(X)
\mvdash{}  (f  x)  =  (g  x)


By

---

Latex:
((InstLemma  `dlattice-eq-equiv`  [\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (newQuotientElim  (-2)  \mcdot{}  THENA  Auto)
  THEN  (Subst'  bs  =  as  0  THENA  (Try  (EqTypeCD)  THEN  Auto))
  THEN  ThinVar  `bs'
  THEN  Thin  (-1))

---

Home Index