proposition: Lemma domain_single_empty y v xs : domain xs (single y v) [=] empty <-> ~In y xs \/ v = Var y.
proof: Proof. rewrite domain_single. case_eq (mem y xs && negb (beq_term v (Var y))). rewrite andb_true_iff, <- mem_iff, negb_true_iff, beq_term_false_iff. intros [h1 h2]. split. 2: fo. intro e. absurd (In y empty). set_iff. fo. rewrite <- e. set_iff. refl. rewrite andb_false_iff, <- not_mem_iff, negb_false_iff, beq_term_true_iff. intros [h1|h2]; split. fo. refl. right. hyp. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)