proposition: Lemma In_domain x s : forall xs, In x (domain xs s) <-> In x xs /\ s x <> Var x.
proof: Proof. apply set_induction_bis. intros xs xs' xsxs' h. rewrite <- xsxs', h. refl. rewrite domain_empty. set_iff. tauto. intros y xs n IH. rewrite domain_add. set_iff. 2: hyp. unfold Def.domain_fun, bool_of_rel. destruct (eq_term_dec (s y) (Var y)); set_iff; rewrite IH; split. tauto. intros [[h1|h1] h2]; subst; tauto. intros [h1|h1]; subst; tauto. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)