proposition: Lemma bv_rename x y : forall u, ~In y (bv u) -> bv (rename x y u) [=] bv u.
proof: Proof. induction u. simpl. intros _. unfold Def.rename. simpl. unfold Def.single, Def.update. eq_dec x0 x; refl. refl. rewrite rename_app. simpl. set_iff. intro n. rewrite IHu1, IHu2. refl. tauto. tauto. unfold Def.rename in *. simpl. set_iff. intro n. rewrite var_rename. case_eq (mem x (fv u) && negb (eqb x0 x) && eqb x0 y). rewrite andb_true_iff, eqb_true_iff. tauto. rewrite !andb_false_iff. eq_dec x0 x. subst x0. simpl. bool. rewrite update_single_eq, single_id. refl. simpl. bool. eq_dec y x0. firstorder auto with exfalso. bool. rewrite update_id, IHu. refl. tauto. rewrite single_neq. refl. fo. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)