proposition: Lemma domain_single y v : forall xs, domain xs (single y v) [=] if mem y xs && negb (beq_term v (Var y)) then singleton y else empty.
proof: Proof. apply set_induction_bis. intros xs xs' xsxs'. rewrite xsxs'. auto. rewrite domain_empty, empty_b. refl. intros x xs n IH. rewrite domain_add, add_b, IH. 2: hyp. clear IH. unfold eqb, Def.domain_fun. unfold bool_of_rel at 1. destruct (eq_term_dec (single y v x) (Var x)). revert e. unfold Def.single, Def.update. eq_dec x y; intro h. subst. rewrite not_mem_iff in n. rewrite n, beq_term_refl. refl. refl. unfold bool_of_rel. revert n0. unfold Def.single, Def.update. eq_dec x y; simpl. 2: tauto. subst. destruct (mem y xs); destruct (eq_term_dec v (Var y)); simpl. tauto. rewrite singleton_equal_add, add_equal. refl. set_iff. auto. tauto. rewrite singleton_equal_add. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)