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