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