proposition: Lemma subs_notin_fv u s : domain (fv u) s [=] empty -> subs s u = u.
proof: Proof. rewrite empty_subset. revert u s. induction u; simpl; intro s. rewrite singleton_equal_add, domain_add. 2: set_iff; auto. rewrite domain_empty. unfold Def.domain_fun, bool_of_rel. destruct (eq_term_dec (s x) (Var x)). auto. intro h. cut False. tauto. rewrite <- empty_iff, <- h. apply add_1. refl. refl. intro h. rewrite IHu1, IHu2. refl. rewrite (@union_subset_2 (fv u1) (fv u2)). hyp. rewrite (@union_subset_1 (fv u1) (fv u2)). hyp. intro h. unfold Def.var; ens. set (xs := fvcodom (remove x (fv u)) s). case_eq (mem x xs); intro hx. rewrite <- mem_iff in hx. unfold xs in hx. rewrite In_fvcodom in hx. destruct hx as [z hz]. gen (h z). set_iff. intro a. cut False. tauto. apply a. revert hz. repeat (rewrite In_domain; set_iff). intuition. f_equal. apply IHu. intro y. gen (h y). do 2 rewrite In_domain. set_iff. unfold Def.update. eq_dec y x. subst y. intuition. intuition. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)