proposition: Lemma fvcod_singleton s x : fvcod (singleton x) s [=] fv (s x).
proof: Proof. intro y. split; rewrite In_fvcod. intros [z [h1 h2]]. revert h1. set_iff. intro e. subst z. hyp. intro h. ex x. set_iff. fo. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)