---

Step * 1 of Lemma sub-co-list_transitivity


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)
BY
{ (D 0 With ⌜combine-skips(n1;ns;0)⌝  THEN Auto) }

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)
⊢ s1 = s3@combine-skips(n1;ns;0) ∈ colist(T)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [s1]  :  colist(T)
3.  [s2]  :  colist(T)
4.  [s3]  :  colist(T)
5.  ns  :  colist(\mBbbN{})
6.  s1  =  s2@ns
7.  n1  :  colist(\mBbbN{})
8.  s2  =  s3@n1
\mvdash{}  sub-co-list(T;s1;s3)


By

---

Latex:
(D  0  With  \mkleeneopen{}combine-skips(n1;ns;0)\mkleeneclose{}    THEN  Auto)

---

Home Index