proposition: Lemma rename_subs_com x y : forall u s, s x = Var x -> s y = Var y -> ~In x (fvcodom (fv u) s) -> inter (bv u) (add y (fvcodom (fv u) s)) [=] empty -> rename x y (subs s u) = subs s (rename x y u).
proof: Proof. induction u; intros s hx hy. rename x0 into z. simpl. rewrite fvcodom_singleton, rename_var. unfold bool_of_rel. destruct (eq_term_dec (s z) (Var z)). rewrite e, rename_var. eq_dec z x; auto. intro h. unfold Def.rename. rewrite single_notin_fv. 2: hyp. eq_dec z x; simpl. subst z. tauto. refl. refl. simpl. rewrite fvcodom_union, union_inter_1, union_empty. set_iff. intros h1 [h2 h3]. rewrite rename_app, IHu1, IHu2; auto; rewrite empty_subset. rewrite union_subset_2 with (s':=fvcodom (fv u2) s) (s:=fvcodom (fv u1) s). rewrite <- empty_subset. hyp. rewrite union_subset_1 with (s':=fvcodom (fv u2) s) (s:=fvcodom (fv u1) s). rewrite <- empty_subset. hyp. rename x0 into z. simpl Def.bv. intros h1 h2. rewrite rename_lam. case_eq (mem x (fv u) && negb (eqb y x) && eqb y z). rewrite !andb_true_iff, eqb_true_iff. intros [[i1 i2] i3]. subst z. revert h2. rewrite add_union_singleton, union_inter_1, union_empty, singleton_equal_add, inter_add_1, inter_empty_l. intros [h _]. gen (h y). set_iff. tauto. set_iff. auto. rewrite !andb_false_iff. intros [[i|i]|i]. eq_dec z x. subst. apply rename_notin_fv. rewrite fv_subs. simpl in *. set_iff. tauto. rewrite rename_notin_fv with (u:=u). 2: rewrite not_mem_iff; hyp. apply rename_notin_fv. rewrite fv_subs. simpl in *. set_iff. unfold Def.fvcodom in h1. rewrite <- not_mem_iff in i. intuition. revert i. rewrite negb_false_iff, eqb_true_iff. intro i. subst y. rewrite !rename_id. eq_dec z x; refl. eq_dec z x. subst. apply rename_notin_fv. rewrite fv_subs. simpl in *. set_iff. tauto. rewrite !subs_lam_no_alpha. set (s' := update z (Var z) s). rewrite <- IHu, rename_lam, i, !andb_false_r. rewrite <- eqb_false_iff in n. rewrite n. refl. unfold s'. unfold Def.update. eq_dec x z. subst. refl. hyp. unfold s'. unfold Def.update. eq_dec y z. subst. refl. hyp. rewrite In_fvcodom. intros [b [j1 [j2 j3]]]. apply h1. rewrite In_fvcodom. exists b. simpl. set_iff. revert j2 j3. unfold s'. unfold Def.update. eq_dec b z. subst. tauto. intuition. assert (e : fvcodom (fv u) s' [=] fvcodom (fv (Lam z u)) s). intro a. rewrite !In_fvcodom. split; intros [b [j1 [j2 j3]]]; exists b; simpl in *; revert j1 j2 j3; set_iff; unfold s'; unfold Def.update; eq_dec b z. subst. tauto. split_all. subst. tauto. tauto. rewrite e. revert h2. rewrite !empty_subset, add_union_singleton. intro h2. rewrite union_subset_2 with (s:=singleton z) (s':=bv u). hyp. assert (e : fvcodom (remove z (fv (rename x y u))) s [=] fvcodom (fv (Lam z u)) s). intro a. rewrite !In_fvcodom. split; intros [b [j1 [j2 j3]]]; exists b; revert j1 j2 j3; set_iff; rewrite fv_rename; unfold replace; case_eq (mem x (fv u)); simpl; set_iff; intros ??? H2; split_all. subst b. revert H2. rewrite hy. simpl. set_iff. intro e. subst a. tauto. right. split. hyp. intro h. subst b. tauto. rewrite e. rewrite inter_empty in h2. gen (h2 z). set_iff. tauto. rewrite inter_empty in h2. gen (h2 z). set_iff. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)