proposition: Lemma mem_domain x s xs : mem x (domain xs s) = mem x xs && negb (beq_term (s x) (Var x)).
proof: Proof. rewrite eqb_equiv, andb_true_iff, negb_true_iff, beq_term_false_iff. rewrite <- !mem_iff. apply In_domain. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)