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