---

Step * of Lemma sub-co-list_transitivity

∀[T:Type]. ∀[s1,s2,s3:colist(T)].  (sub-co-list(T;s1;s2) ⇒ sub-co-list(T;s2;s3) ⇒ sub-co-list(T;s1;s3))
BY
{ (Auto THEN D -2 THEN D -1) }

1
1. [T] : Type
2. [s1] : colist(T)
3. [s2] : colist(T)
4. [s3] : colist(T)
5. ns : colist(ℕ)
6. s1 = s2@ns ∈ colist(T)
7. n1 : colist(ℕ)
8. s2 = s3@n1 ∈ colist(T)
⊢ sub-co-list(T;s1;s3)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[s1,s2,s3:colist(T)].
    (sub-co-list(T;s1;s2)  {}\mRightarrow{}  sub-co-list(T;s2;s3)  {}\mRightarrow{}  sub-co-list(T;s1;s3))


By

---

Latex:
(Auto  THEN  D  -2  THEN  D  -1)

---

Home Index