proposition: Lemma In_fvcodom s xs y : In y (fvcodom xs s) <-> (exists x, In x xs /\ s x <> Var x /\ In y (fv (s x))).
proof: Proof. unfold Def.fvcodom. rewrite In_fvcod. intuition; destruct H as [x hx]; exists x; rewrite In_domain in *; tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)