proposition: Lemma update_single_split : forall u x y v w, x<>y -> ~In y (fv v) -> inter (bv u) (union (fv v) (fv w)) [=] empty -> subs (update y w (single x v)) u = subs (single y w) (subs (single x v) u).
proof: Proof. induction u; intros x' y v w n hy h. simpl. unfold Def.update. eq_dec x y. subst y. rewrite single_neq. 2: auto. simpl. sym. apply single_eq. unfold Def.single at -2. unfold Def.update. sym. eq_dec x x'. apply single_notin_fv. hyp. simpl. apply single_neq. auto. refl. revert h. simpl. rewrite union_inter_1, union_empty. intros [a b]. rewrite IHu1, IHu2; tauto. revert h. simpl Def.bv. rewrite inter_empty. intro h. assert (hx : ~In x (union (fv v) (fv w))). apply h. set_iff. auto. revert hx; set_iff; intro hx. assert (~In x (fv v) /\ ~In x (fv w)). tauto. clear hx. rewrite subs_lam_no_alpha. 2:{ unfold not. rewrite In_fvcodom. intros [z hz]. revert hz. set_iff. unfold Def.single, Def.update. eq_dec z y; eq_dec z x'; subst; tauto. } rewrite !single_lam_no_alpha; try tauto. f_equal. eq_dec x' x. subst x'. rewrite update2_neq_com. 2: hyp. rewrite update2_single_eq, update_single_eq, single_id. apply subs_seq. intros z hz. unfold Def.single, Def.update. eq_dec z y; eq_dec z x; try refl. subst. subst. tauto. eq_dec x y. subst. rewrite update2_eq, update_id_single. 2: auto. rewrite update_single_eq, single_id. refl. rewrite update_id. 2:{ unfold Def.single, Def.update. eq_dec x y; eq_dec x x'; subst; tauto. } rewrite update_id. 2:{ unfold Def.single, Def.update. eq_dec x y; subst; tauto. } rewrite update_id. 2:{ rewrite single_neq; auto. } apply IHu. hyp. hyp. intro z. gen (h z). set_iff. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)