---

Step * of Lemma dlattice-eq-equiv

∀[X:Type]. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
BY
{ (Auto
   THEN (RepeatFor 2 (D 0) THEN Auto)
   THEN RepUR ``dlattice-eq`` 0
   THEN Auto
   THEN Try ((BLemma `dlattice-order_weakening` THEN Auto))
   THEN D 0
   THEN Auto) }

1
1. [X] : Type
2. a : X List List
3. b : X List List
4. c : X List List
5. a ⇒ b
6. b ⇒ a
7. b ⇒ c
8. c ⇒ b
⊢ a ⇒ c

2
1. [X] : Type
2. a : X List List
3. b : X List List
4. c : X List List
5. a ⇒ b
6. b ⇒ a
7. b ⇒ c
8. c ⇒ b
9. a ⇒ c
⊢ c ⇒ a

---

Latex:

---

Latex:
\mforall{}[X:Type].  EquivRel(X  List  List;as,bs.dlattice-eq(X;as;bs))


By

---

Latex:
(Auto
  THEN  (RepeatFor  2  (D  0)  THEN  Auto)
  THEN  RepUR  ``dlattice-eq``  0
  THEN  Auto
  THEN  Try  ((BLemma  `dlattice-order\_weakening`  THEN  Auto))
  THEN  D  0
  THEN  Auto)

---

Home Index