proposition: Lemma single_com x y v w : x<>y -> forall u, ~In x (fv w) \/ ~In y (fv u) -> inter (bv u) (union (fv v) (fv w)) [=] empty -> subs (single y w) (subs (single x v) u) = subs (single x (subs (single y w) v)) (subs (single y w) u).
proof: Proof. intro n. induction u. simpl. set_iff. intros h _. unfold Def.single at 5. unfold Def.update. eq_dec x0 y. subst x0. rewrite single_notin_fv with (v:=w). 2: tauto. rewrite single_neq. 2: hyp. simpl. apply single_eq. simpl. unfold Def.single at 2. unfold Def.single at 2. unfold Def.update. eq_dec x0 x. refl. simpl. apply single_neq. auto. refl. simpl. set_iff. intro h. rewrite union_inter_1, union_empty. intros [a b]. rewrite IHu1, IHu2; split_all. simpl Def.fv. simpl Def.bv. set_iff. rewrite inter_empty. intros h1 h2. assert (h3 : ~In x0 (union (fv v) (fv w))). apply h2. set_iff. auto. revert h3. set_iff. intro h3. rewrite !single_lam_no_alpha. f_equal. eq_dec x0 x. subst. repeat rewrite update_single_eq, single_id; auto. eq_dec x0 y. subst. repeat rewrite update_single_eq, single_id; auto. rewrite !update_id_single; auto. rewrite single_notin_fv with (v:=v); auto. rewrite !update_id_single; auto. rewrite IHu. refl. revert h1. simpl. set_iff. tauto. rewrite inter_empty. intros a ha. apply h2. set_iff. auto. eq_dec x0 x. auto. eq_dec x0 y. subst. rewrite update_single_eq, single_id. rewrite single_notin_fv; auto. clear IHu; tauto. rewrite update_id_single; auto. rewrite !fv_single. case_eq (mem y (fv v)); intro hyv; set_iff; clear IHu; tauto. clear IHu; tauto. 2: clear IHu; tauto. eq_dec x0 x. subst. rewrite update_single_eq, single_id. tauto. rewrite update_id_single; auto. rewrite fv_single. case_eq (mem x (fv u)); intro hx; set_iff; clear IHu; tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)