proposition: Lemma up_upren_n_internal : (forall xi, up (ren xi) = ren (upren xi)) -> (forall xi n, upn n (ren xi) = ren (iterate upren n xi)).
proof: Proof. apply (iter_param upren up (fun x => ren x)). Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas