proposition: Lemma domain_id : forall xs, domain xs id [=] empty.
proof: Proof. apply set_induction_bis. intros xs xs' xsxs' h. rewrite <- xsxs'. hyp. apply domain_empty. intros x xs n IH. rewrite domain_add. 2: hyp. unfold Def.domain_fun, bool_of_rel. destruct (eq_term_dec (id x) (Var x)). hyp. absurd (id x=Var x); tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)