proposition: Lemma fvcod_id : forall xs, fvcod xs id [=] xs.
proof: Proof. apply set_induction_bis. intros xs xs' xsxs' h. rewrite <- xsxs'. hyp. apply fvcod_empty. intros x xs n IH. rewrite fvcod_add. 2: hyp. unfold Def.fvcod_fun. simpl. rewrite IH. intro a. set_iff. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)