proposition: Lemma hcomp_lift_internal sigma theta : (sigma >>| theta) >>| ren (+1) = (sigma >>| ren (+1)) >>| up theta.
proof: Proof. apply hcomp_lift_n_internal. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas