proposition: Lemma bvcod_single y v : forall xs, bvcod xs (single y v) [=] if mem y xs then bv v else empty.
proof: Proof. apply set_induction_bis. intros s s' ss'. rewrite ss'. auto. rewrite bvcod_empty, empty_b. refl. intros x u n IH. rewrite bvcod_add, IH. 2: hyp. clear IH. unfold bvcod_fun. unfold Def.single, Def.update, eqb. eq_dec x y; rewrite add_b. subst y. rewrite eqb_refl. simpl. rewrite not_mem_iff in n. rewrite n. intro a; set_iff; tauto. rewrite <- eqb_false_iff in n0. rewrite n0. simpl. intro a; set_iff; tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)