(* Note: this requires ↑ on first n *)
(*** after_tls *)
lemma pr_after_tls_sn_tls (n):
- â\88\80f1,f2,f. @â\9dªð\9d\9f\8f, f1â\9d« ≘ ↑n →
+ â\88\80f1,f2,f. @â\9d¨ð\9d\9f\8f, f1â\9d© ≘ ↑n →
f1 ⊚ f2 ≘ f → ⫰*[n]f1 ⊚ f2 ≘ ⫰*[n]f.
#n @(nat_ind_succ … n) -n //
#n #IH #f1 #f2 #f #Hf1 #Hf