proposition: Lemma subs_update x y s u : s y = Var y -> subs (update x (Var y) s) u ~~ subs (update x (Var x) s) (rename x y u).
proof: Proof. intro h. unfold Def.rename. rewrite subs_comp. apply subs_saeq. intros z hz. unfold Def.comp, Def.single. unfold Def.update at -2. eq_dec z x; simpl. subst. unfold Def.update. eq_dec y x. subst. refl. rewrite h. refl. unfold Def.update. eq_dec z x. subst. tauto. refl. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)