proposition: Lemma up_id_internal : (forall xi x, rename xi (ids x) = ids (xi x)) -> up ids = ids :> (var -> term).
proof: Proof. intros h. f_ext. intros [|x]. reflexivity. apply h. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas