(* Constructions with stream_tls ********************************************)
-lemma tr_pap_plus (i1) (i2) (f):
- (⇂*[ninj i2]f)@❨i1❩+f@❨i2❩ = f@❨i1+i2❩.
-#i1 #i2 elim i2 -i2
+lemma tr_pap_plus (p1) (p2) (f):
+ (⇂*[ninj p2]f)@⧣❨p1❩+f@⧣❨p2❩ = f@⧣❨p1+p2❩.
+#p1 #p2 elim p2 -p2
[ * #p #f //
| #i #IH * #p #f
<pplus_succ_dx <tr_pap_succ <tr_pap_succ