proposition: Lemma domain_singleton s x : domain (singleton x) s [=] if beq_term (s x) (Var x) then empty else singleton x.
proof: Proof. intro y. unfold bool_of_rel. destruct (eq_term_dec (s x) (Var x)); rewrite In_domain; set_iff; split. intros [h1 h2]. subst. fo. fo. fo. intro e. subst. fo. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)