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