proposition: Lemma permut_rename v x y u : v ~~ rename x y u -> (x = y \/ ~In y (fv u)) -> u ~~ rename y x v /\ (x = y \/ ~In x (fv v)).
proof: Proof. intros e h. split. rewrite e, rename2, rename_id. refl. hyp. rewrite e, fv_rename; unfold replace. destruct h. auto. subst. auto. case_eq (mem x (fv u)); intro i. 2:{ rewrite <- not_mem_iff in i. auto. } right. set_iff. rewrite <- mem_iff in i. split_all. subst. contr. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)