-lemma tr_compose_tls (i) (f2) (f1):
- (⇂*[f1@❨i❩]f2)∘⇂*[i]f1 = ⇂*[i](f2∘f1).
-#i elim i -i
-[ #f2 * #p1 #f1 //
-| #i #IH #f2 * #p1 #f1
- >nsucc_inj <stream_tls_swap <stream_tls_swap
- <tr_pap_succ >nrplus_inj_dx >nrplus_inj_sn
- <tr_compose_unfold <IH -IH //
-]
+lemma tr_compose_tls (p) (f1) (f2):
+ (⇂*[f1@⧣❨p❩]f2)∘(⇂*[p]f1) = ⇂*[p](f2∘f1).
+#p elim p -p [| #p #IH ] * #q1 #f1 #f2 //
+<tr_compose_unfold <tr_pap_succ
+>nsucc_inj <stream_tls_succ_lcons <stream_tls_succ_lcons
+<IH -IH >nrplus_inj_dx >nrplus_inj_sn <stream_tls_plus //