proposition: Lemma scomp_hcompX sigma theta : subst sigma >>> hsubst theta = hsubst theta >>> subst (sigma >>>hsubst theta).
proof: Proof. f_ext. apply subst_hsubst_comp. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes