proposition: Lemma single_rename x y u v : x = y \/ ~In y (fv u) -> subs (single y v) (rename x y u) ~~ subs (single x v) u.
proof: Proof. intro hy. unfold Def.rename. rewrite subs_comp. apply subs_saeq. intros d hd. unfold Def.comp, Def.single. unfold Def.update at -1. eq_dec d x; simpl. rewrite update_eq. refl. unfold Def.update. eq_dec d y. 2: refl. subst d. assert (n':x<>y). auto. tauto. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)