-lemma after_apply: ∀p1,f2,f1,f.
- (⫰*[ninj p1] f2) ⊚ f1 ≘ f → f2 ⊚ p1⨮f1 ≘ f2@❨p1❩⨮f.
+include "ground/lib/stream_tls.ma".
+include "ground/relocation/tr_pap.ma".
+
+(*** after_apply *)
+lemma tr_after_pap:
+ ∀p1,f2,f1,f. 𝐭❨⇂*[ninj p1]f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f❩ →
+ (𝐭❨f2❩) ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨f2@❨p1❩⨮f❩.