---

Step * 1 of Lemma free-dl-join_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-join(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-join` 0
   THEN EqTypeCD
   THEN Auto) }

1
.....antecedent..... 
1. X : Type
2. X List List ∈ Type
3. ∀a1,b1:X List List.  (dlattice-eq(X;a1;b1) ∈ Type)
4. ∀a1:X List List. dlattice-eq(X;a1;a1)
5. X List List ∈ Type
6. ∀as,b2:X List List.  (dlattice-eq(X;as;b2) ∈ Type)
7. ∀as:X List List. dlattice-eq(X;as;as)
8. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
9. a1 : X List List@i
10. b1 : X List List@i
11. dlattice-eq(X;a1;b1)
12. (as,bs:X List List//dlattice-eq(X;as;bs)) = (as,bs:X List List//dlattice-eq(X;as;bs)) ∈ Type
13. as : X List List@i
14. b2 : X List List@i
15. dlattice-eq(X;as;b2)
16. (as,bs:X List List//dlattice-eq(X;as;bs)) = (as,bs:X List List//dlattice-eq(X;as;bs)) ∈ Type
⊢ dlattice-eq(X;a1 @ as;b1 @ b2)

---

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-join(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-join`  0
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index