proposition: Lemma hcomp_lift_n_internal sigma theta n : (sigma >>| theta) >>| ren (+n) = (sigma >>| ren (+n)) >>| upn n theta.
proof: Proof. f_ext. intros x; simpl. now rewrite !hsubst_comp, up_liftn. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas