(* Constructions with tr_compose and tr_tls *********************************)
+lemma tr_tls_compose_uni_sn (f) (n) (p:pnat):
+ ⇂*[p]f ≗ ⇂*[p](𝐮❨n❩∘f).
+#f #n #p elim p -p //
+#p #IH /2 width=1 by stream_tl_eq_repl/
+qed.
+
lemma tr_tl_compose_uni_dx (f) (n):
⇂*[↑n]f ≗ ⇂(f∘𝐮❨n❩).
// qed.
(* Main constructions with tr_compose and tr_tls ****************************)
-theorem tr_compose_uni_dx (f) (n):
- (𝐮❨f@❨n❩❩∘⇂*[n]f ≗ f∘𝐮❨n❩).
+theorem tr_compose_uni_dx_pap (f) (p):
+ (𝐮❨f@⧣❨p❩❩∘⇂*[p]f) ≗ f∘𝐮❨p❩.
#f #p
@nstream_eq_inv_ext #q
<tr_compose_pap <tr_compose_pap