proposition: Lemma subs1_no_alpha : forall u s, inter (bv u) (fvcodom (fv u) s) [=] empty -> subs s u = subs1 s u.
proof: Proof. induction u; intro s; simpl; auto. rewrite fvcodom_union, union_inter_1, union_empty, inter_sym, inter_sym with (s:=bv u2). rewrite !union_inter_1, !union_empty. split_all. rewrite IHu1, IHu2; try rewrite inter_sym; auto. rewrite inter_empty. intro h1. assert (i : mem x (fvcodom (remove x (fv u)) s) = false). rewrite <- not_mem_iff. apply h1. set_iff. auto. assert (j : var x u s = x). unfold Def.var; ens. rewrite i. refl. rewrite j, IHu. refl. rewrite empty_subset. intro y. set_iff. intros [i1 i2]. eapply h1. set_iff. right. apply i1. rewrite <- fvcodom_update_id. hyp. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)