proposition: Lemma seq_restrict xs ys s : xs [<=] ys -> seq xs s (restrict ys s).
proof: Proof. intros i x. rewrite i, mem_iff. intro h. unfold Def.restrict; ens. rewrite h. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)