lemma pippo (f):
      f@❨𝟏❩⨮⇂f = f.
* #p #f //
qed.

corec lemma tr_compose_id_dx (f):
            f ≗ f∘𝐢.
cases tr_id_unfold
cases tr_compose_unfold
cases (pippo f) in ⊢ (??%?);
@stream_eq_cons /2 width=1 by/
qed.

axiom pippo2 (f) (p):
      f@❨p❩ + (⇂*[ninj p]f)@❨𝟏❩ = f@❨↑p❩.

lemma tr_uni_tl (n):
      (𝐢) = ⇂𝐮❨n❩.
// qed.

axiom tr_uni_tls_pos (p:pnat) (n):
      (𝐢) = ⇂*[p]𝐮❨n❩.
(*
#p #n
>nsucc_pnpred <stream_tls_swap
<tr_uni_tl <tr_id_tls
// qed.
*)