proposition: Lemma In_bvcod y s : forall xs, In y (bvcod xs s) <-> exists x, In x xs /\ In y (bv (s x)).
proof: Proof. apply set_induction_bis. intros xs xs' xsxs' h. rewrite <- xsxs', h. clear h. intuition; destruct H as [x]; exists x; [rewrite <- xsxs'|rewrite xsxs']; hyp. rewrite bvcod_empty. set_iff. intuition. destruct H as [x]. revert H. set_iff. tauto. intros x xs n IH. rewrite bvcod_add. 2: hyp. unfold bvcod_fun. set_iff. rewrite IH. clear IH. split. intros [h|[a [a1 a2]]]. ex x. split; set_iff; auto. ex a. split; set_iff; auto. intros [a [a1 a2]]. eq_dec a x. subst. auto. right. ex a. split. revert a1. set_iff. firstorder auto with exfalso. hyp. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)