proposition: Lemma bvcod_seq xs xs' : xs [=] xs' -> forall s s', seq xs s s' -> bvcod xs s [=] bvcod xs' s'.
proof: Proof. intros e s s' ss' x. rewrite <- e. rewrite !In_bvcod. split; intros [y [h1 h2]]; exists y. rewrite <- (ss' _ h1). tauto. rewrite (ss' _ h1). tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)