proposition: Lemma up_comp_n sigma tau n : upn n sigma >> upn n tau = upn n (sigma >> tau).
proof: Proof. induction n; [reflexivity|now rewrite !iterate_S, <- IHn, up_comp]. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics