proposition: Lemma scomp_hcompR {A} sigma theta (f : _ -> A) : subst sigma >>> (hsubst theta >>> f) = hsubst theta >>> (subst (sigma >>> hsubst theta) >>> f).
proof: Proof. now rewrite <- compA, scomp_hcompX. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes