---

Step * 1 of Lemma free-dl-meet_wf


1. [X] : Type
2. [as] : free-dl-type(X)
3. [bs] : free-dl-type(X)
4. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
⊢ free-dl-meet(as;bs) ∈ free-dl-type(X)
BY
{ (All (Unfold `free-dl-type`)
   THEN (newQuotientElim 2 THEN Auto)
   THEN newQuotientElim 5
   THEN Auto
   THEN Unfold `free-dl-meet` 0
   THEN EqTypeCD
   THEN Auto
   THEN Fold `free-dl-meet` 0
   THEN All (Unfold `dlattice-eq`)
   THEN D 0
   THEN EAuto 1) }

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  [as]  :  free-dl-type(X)
3.  [bs]  :  free-dl-type(X)
4.  EquivRel(X  List  List;as,bs.dlattice-eq(X;as;bs))
\mvdash{}  free-dl-meet(as;bs)  \mmember{}  free-dl-type(X)


By

---

Latex:
(All  (Unfold  `free-dl-type`)
  THEN  (newQuotientElim  2  THEN  Auto)
  THEN  newQuotientElim  5
  THEN  Auto
  THEN  Unfold  `free-dl-meet`  0
  THEN  EqTypeCD
  THEN  Auto
  THEN  Fold  `free-dl-meet`  0
  THEN  All  (Unfold  `dlattice-eq`)
  THEN  D  0
  THEN  EAuto  1)

---

Home Index