---

Step * 1 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)
⊢ s1 = s3@combine-skips(n1;ns;0) ∈ colist(T)
BY
{ (RWO "list-at-at<" 0 THEN Auto) }

---

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{}  s1  =  s3@combine-skips(n1;ns;0)


By

---

Latex:
(RWO  "list-at-at<"  0  THEN  Auto)

---

Home Index