proposition: Lemma up_comp_subst_ren_internal : (forall xi x, rename xi (ids x) = ids (xi x)) -> (forall xi s, rename xi s = s.[ren xi]) -> (forall xi sigma s, (rename xi s).[sigma] = s.[xi >>> sigma]) -> (forall sigma xi, up (sigma >>> rename xi) = up sigma >>> rename (upren xi)).
proof: Proof. intros h1 h2 h3 sigma xi. f_ext. intros [|x]. unfold up; simpl. now rewrite h1. unfold up. simpl. now rewrite h2, h3, h2, h3. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas