proposition: Lemma var_rename y z x u : var x u (single y (Var z)) = if mem y (fv u) && negb (eqb x y) && eqb z x then var_notin (add z (fv u)) else x.
proof: Proof. rewrite var_single, beq_term_var. simpl. rewrite singleton_b. case_eq (mem y (fv u) && negb (eqb x y) && eqb z x). rewrite !andb_true_iff. intros [[h1 h2] h3]. rewrite h1, h2, h3. simpl. rewrite eqb_true_iff in h3. subst z. rewrite h2. simpl. apply var_notin_e. intro a. set_iff. tauto. rewrite !andb_false_iff. intros [[h|h]|h]; rewrite h; repeat rewrite andb_false_r; refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)