proposition: Lemma fvcod_union s p q : fvcod (union p q) s [=] union (fvcod p s) (fvcod q s).
proof: Proof. intro x. rewrite In_fvcod. set_iff. split. intros [y [h1 h2]]. revert h1. set_iff. rewrite !In_fvcod. intros [h1|h1]. left. ex y. fo. right. ex y. fo. rewrite !In_fvcod. intros [[y [h1 h2]]|[y [h1 h2]]]. ex y. set_iff. fo. ex y. set_iff. fo. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)