---

Step * 1 1 of Lemma free-dl-join_wf

.....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)
BY
{ (Lemmaize [-6;-2] THEN Auto) }

1
1. X : Type@i'
2. a1 : X List List@i
3. b1 : X List List@i
4. as : X List List@i
5. b2 : X List List@i
6. dlattice-eq(X;a1;b1)
7. dlattice-eq(X;as;b2)
⊢ dlattice-eq(X;a1 @ as;b1 @ b2)

---

Latex:

---

Latex:
.....antecedent..... 
1.  X  :  Type
2.  X  List  List  \mmember{}  Type
3.  \mforall{}a1,b1:X  List  List.    (dlattice-eq(X;a1;b1)  \mmember{}  Type)
4.  \mforall{}a1:X  List  List.  dlattice-eq(X;a1;a1)
5.  X  List  List  \mmember{}  Type
6.  \mforall{}as,b2:X  List  List.    (dlattice-eq(X;as;b2)  \mmember{}  Type)
7.  \mforall{}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))
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))
\mvdash{}  dlattice-eq(X;a1  @  as;b1  @  b2)


By

---

Latex:
(Lemmaize  [-6;-2]  THEN  Auto)

---

Home Index