proposition: Lemma up_liftn sigma n : ren (+n) >> upn n sigma = sigma >> ren (+n).
proof: Proof. f_ext. intros x. simpl. rewrite id_subst. induction n. - autosubst. - rewrite !iterate_S, upE. simpl. rewrite IHn. autosubst. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics