proposition: Lemma bvcod_union s p q : bvcod (union p q) s [=] union (bvcod p s) (bvcod q s).
proof: Proof. intro x. rewrite In_bvcod. set_iff. split. intros [y [h1 h2]]. revert h1. set_iff. rewrite !In_bvcod. intros [h1|h1]. left. exists y. intuition. right. exists y. intuition. rewrite !In_bvcod. intros [[y [h1 h2]]|[y [h1 h2]]]. exists y. set_iff. tauto. exists y. set_iff. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)