+
+lemma tr_xap_plus (n1) (n2) (f):
+ (⇂*[n2]f)@❨n1❩+f@❨n2❩ = f@❨n1+n2❩.
+* [| #n1 ] // * [| #n2 ] // #f
+<nrplus_inj_sn <nrplus_inj_dx
+<nrplus_inj_sn <nrplus_inj_dx
+>tr_pap_plus //
+qed.
+
+theorem tr_xap_eq_repl (i):
+ stream_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
+#i #f1 #f2 #Hf
+<tr_xap_unfold <tr_xap_unfold
+/3 width=1 by tr_push_eq_repl, tr_nap_eq_repl/
+qed.
+
+lemma tr_nap_plus (f) (m) (n):
+ ⇂*[↑n]f@❨m❩+f@§❨n❩ = f@§❨m+n❩.
+/2 width=1 by eq_inv_nsucc_bi/
+qed.
+
+lemma tr_xap_pos (f) (n):
+ n = ↑↓n → f@❨n❩=↑↓(f@❨n❩).
+#f #n #H0 >H0 -H0
+<tr_xap_ninj <nsucc_pnpred //
+qed.