proposition: Lemma bvcod_add s x xs : ~In x xs -> bvcod (add x xs) s [=] bvcod_fun s x (bvcod xs s).
proof: Proof. intro n. unfold bvcod. rewrite fold_add. refl. apply Equal_ST. apply bvcod_fun_e. refl. apply bvcod_fun_transp. hyp. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)