proposition: Lemma single_notin_fv y u v : ~In y (fv v) -> subs (single y u) v = v.
proof: Proof. intro n. rewrite subs_notin_fv. refl. intro x. rewrite In_domain. set_iff. unfold Def.single, Def.update. eq_dec x y. subst x. intuition. intuition. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)