proposition: Lemma fold_up k sigma : ids k .: sigma >> ren (+S k) = up sigma >> ren (+k).
proof: Proof. unfold scomp, ren. rewrite upX; fsimpl; rewrite id_subst, subst_compX; simpl; fsimpl. unfold ren. fsimpl. rewrite id_scompX. now fsimpl. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes