proposition: Lemma hcomp_dist_internal sigma tau theta : (sigma >> tau) >>| theta = (sigma >>| theta) >> (tau >>| theta).
proof: Proof. f_ext. intros x. simpl. apply subst_hsubst_comp. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas