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