proposition: Lemma notin_domain s xs x : domain xs s [=] empty -> In x xs -> s x = Var x.
proof: Proof. intros h1 h2. destruct (eq_term_dec (s x) (Var x)). hyp. absurd (In x (domain xs s)). rewrite h1. set_iff. tauto. rewrite In_domain. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)