---

Step * of Lemma dlattice-order_transitivity

∀[X:Type]. ∀as,bs,cs:X List List.  (as ⇒ bs ⇒ bs ⇒ cs ⇒ as ⇒ cs)
BY
{ Auto }

1
1. [X] : Type
2. as : X List List
3. bs : X List List
4. cs : X List List
5. as ⇒ bs
6. bs ⇒ cs
⊢ as ⇒ cs

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}as,bs,cs:X  List  List.    (as  {}\mRightarrow{}  bs  {}\mRightarrow{}  bs  {}\mRightarrow{}  cs  {}\mRightarrow{}  as  {}\mRightarrow{}  cs)


By

---

Latex:
Auto

---

Home Index