proposition: Lemma fvcodom_singleton s x : fvcodom (singleton x) s [=] if beq_term (s x) (Var x) then empty else fv (s x).
proof: Proof. unfold Def.fvcodom. rewrite domain_singleton. unfold bool_of_rel. destruct (eq_term_dec (s x) (Var x)). apply fvcod_empty. apply fvcod_singleton. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)