proposition: Lemma up_comp_ren_subst xi (sigma : var -> term) : up (xi >>> sigma) = upren xi >>> up sigma.
proof: Proof. f_ext. intros [|x]; reflexivity. Qed.
imports: Autosubst_Basics Autosubst_MMap Autosubst_Classes Autosubst_Tactics Autosubst_Lemmas