proposition: Lemma var_single y v x u : var x u (single y v) = if mem y (fv u) && negb (eqb x y) && negb (beq_term v (Var y)) && mem x (fv v) then var_notin (union (fv u) (fv v)) else x.
proof: Proof. unfold Def.var; ens. rewrite fvcodom_single, remove_b, mem_if. case_eq (mem y (fv u) && negb (eqb x y) && negb (beq_term v (Var y)) && mem x (fv v)). rewrite !andb_true_iff. intros [[[h1 h2] h3] h4]. assert (e : fvcodom (remove x (fv u)) (single y v) [=] fv v). rewrite fvcodom_single, remove_b, h1, h2, h3. simpl. refl. rewrite e. refl. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)