proposition: Lemma bvcod_update x u s xs : bvcod xs (update x u s) [=] union (if mem x xs then bv u else empty) (bvcod (remove x xs) s).
proof: Proof. intro y. set_iff. do 2 rewrite In_bvcod. split_all. unfold Def.update in H0. eq_dec x0 x. subst x0. rewrite mem_iff in H. rewrite H. auto. right. exists x0. set_iff. auto. revert H. case_eq (mem x xs); intros hx H. exists x. rewrite <- mem_iff in hx. rewrite update_eq. auto. revert H. set_iff. tauto. revert H. set_iff. intro H. exists x0. unfold Def.update. eq_dec x0 x. subst x0. tauto. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)