proposition: Lemma dom_incl_restrict s xs : dom_incl xs (restrict xs s).
proof: Proof. intro x. rewrite not_mem_iff. intro hx. unfold Def.restrict; ens. rewrite hx. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)