proposition: Lemma rename2 : forall x y z u, x = y \/ ~In y (fv u) -> rename y z (rename x y u) ~~ rename x z u.
proof: Proof. intros x y z u hy. apply single_rename. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)