proposition: Lemma aeq_notin_bv : forall xs u, exists v, u ~~ v /\ inter (bv v) xs [=] empty.
proof: Proof. intro xs. induction u. ex (Var x). split. refl. simpl. rewrite inter_empty_l. refl. ex (Fun f). split. refl. simpl. rewrite inter_empty_l. refl. destruct IHu1 as [v1 [h1 i1]]. destruct IHu2 as [v2 [h2 i2]]. ex (App v1 v2). split. trans (App v1 u2). apply aeq_app_l. hyp. apply aeq_app_r. hyp. simpl. rewrite union_inter_1, i1, i2, union_empty_l. refl. destruct IHu as [v [h i]]. set (uxs := union (fv v) (union (bv v) xs)). set (x' := var_notin uxs). ex (Lam x' (rename x x' v)). gen (var_notin_ok uxs). fold x'. unfold uxs. set_iff. intro n. split. trans (Lam x v). apply aeq_lam. hyp. apply aeq_alpha. tauto. simpl. rewrite bv_rename. 2: tauto. revert i. rewrite inter_sym at 1. rewrite !inter_empty. unfold not. intros i z. set_iff. intros [j|j]. subst z. tauto. intro hz. eapply i. apply hz. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)