proposition: Lemma bvcod_id : forall xs, bvcod xs id [=] empty.
proof: Proof. apply set_induction_bis. intros xs xs' xsxs' h. rewrite <- xsxs'. hyp. apply bvcod_empty. intros x xs n IH. rewrite bvcod_add. 2: hyp. unfold bvcod_fun. simpl. rewrite IH. fset. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)