proposition: Lemma fvcod_add s x xs : ~In x xs -> fvcod (add x xs) s [=] fvcod_fun s x (fvcod xs s).
proof: Proof. intro n. unfold Def.fvcod. rewrite fold_add. refl. apply Equal_ST. apply fvcod_fun_e. refl. apply fvcod_fun_transp. hyp. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)