lemma pippo (f):
      f@❨𝟏❩⨮⇂f = f.
* #p #f //
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.
*)