proposition: Lemma up_comp_n_internal : (forall sigma tau, up (sigma >> tau) = up sigma >> up tau) -> (forall sigma tau n, upn n (sigma >> tau) = upn n sigma >> upn n tau).
proof: Proof. intros h sigam tau n. induction n. reflexivity. rewrite !iterate_S, IHn. apply h. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas