proposition: Lemma up_comp_subst_ren_n_internal : (forall sigma xi, up (sigma >>> rename xi) = up sigma >>> rename (upren xi))-> (forall (sigma : var -> term) xi n, upn n (sigma >>> rename xi) = upn n sigma >>> rename (iterate upren n xi)).
proof: Proof. intros E sigma xi n. induction n. reflexivity. rewrite !iterate_S, IHn. apply E. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas