proposition: Lemma bvcod_singleton s x : bvcod (singleton x) s [=] bv (s x).
proof: Proof. intro y. split; rewrite In_bvcod. intros [z [h1 h2]]. revert h1. set_iff. intro e. subst z. hyp. intro h. exists x. set_iff. intuition. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)