proposition: Lemma hsubst_compR {A} sigma tau (f : _ -> A) : hsubst sigma >>> (hsubst tau >>> f) = hsubst (sigma >>> subst tau) >>> f.
proof: Proof. now rewrite <- hsubst_compX. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes