proposition: Lemma hcomp_ren_internal sigma xi theta : (forall xi s, rename xi s = s.[ren xi]) -> (sigma >>> rename xi) >>| theta = (sigma >>| theta) >>> rename xi.
proof: Proof. intros E. f_ext. intros x. simpl. rewrite !E, subst_hsubst_comp. f_equal. f_ext. intros y. simpl. now rewrite id_hsubst. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas