-lemma after_fwd_tls: ∀f,f2,n2,f1,n1,n. n1@f1 ⊚ n2@f2 ≡ n@f →
- (â\86\93*[n2]f1) â\8a\9a f2 â\89¡ f.
-#f #f2 #n2 elim n2 -n2
-[ #f1 #n1 #n #H elim (after_inv_xpx … H) -H //
-| #n2 #IH * #m1 #f1 #n1 #n #H elim (after_inv_xnx … H) -H [2,3: // ]
+lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f →
+ (â«°*[n1]f2) â\8a\9a f1 â\89\98 f.
+#f #f1 #n1 elim n1 -n1
+[ #f2 #n2 #n #H elim (after_inv_xpx … H) -H //
+| #n1 #IH * #m1 #f2 #n2 #n #H elim (after_inv_xnx … H) -H [2,3: // ]