proposition: Lemma In_fvcod y s : forall xs, In y (fvcod xs s) <-> exists x, In x xs /\ In y (fv (s x)).
proof: Proof. apply set_induction_bis. intros xs xs' xsxs' h. rewrite <- xsxs', h. clear h. split; intros [x [x1 x2]]; ex x; split; auto. rewrite <- xsxs'. hyp. rewrite xsxs'. hyp. rewrite fvcod_empty. set_iff. intuition. destruct H as [x]. revert H. set_iff. tauto. intros x xs n IH. rewrite fvcod_add. 2: hyp. unfold Def.fvcod_fun. set_iff. rewrite IH. clear IH. split. intros [h|[a [a1 a2]]]. ex x. set_iff. fo. ex a. set_iff. fo. intros [a [a1 a2]]. revert a1. set_iff. intros [a1|a1]. subst. left. hyp. right. ex a. fo. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)