proposition: Lemma up_hcomp_internal : (forall xi theta s, rename xi s.|[theta] = (rename xi s).|[theta]) -> (forall sigma theta, up (sigma >>| theta) = up sigma >>| theta).
proof: Proof. intros E sigma theta. f_ext. intros [|x]; unfold up; simpl. now rewrite id_hsubst. apply E. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas