---

Step * 2 of Lemma dlattice-eq-equiv


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
BY
{ (FLemma `dlattice-order_transitivity` [-4;-2] THEN Auto) }

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  a  :  X  List  List
3.  b  :  X  List  List
4.  c  :  X  List  List
5.  a  {}\mRightarrow{}  b
6.  b  {}\mRightarrow{}  a
7.  b  {}\mRightarrow{}  c
8.  c  {}\mRightarrow{}  b
9.  a  {}\mRightarrow{}  c
\mvdash{}  c  {}\mRightarrow{}  a


By

---

Latex:
(FLemma  `dlattice-order\_transitivity`  [-4;-2]  THEN  Auto)

---

Home Index