proposition: Theorem binds_update_one_neq : forall A x y (v w : A) (F : gen_env A), x ∹ v ⋲ F -> x <> y -> x ∹ v ⋲ (F [y <- w]).
proof: Proof. intros A x y v w F Hbind Hneq. induction F as [ | F z u ] using env_ind. apply binds_empty in Hbind. inversion Hbind. apply binds_concat_inv in Hbind. destruct Hbind as [ Hbind_r | Hbind_l ]. apply binds_single_inv in Hbind_r. destruct Hbind_r as [ Heq1 Heq2 ]. rewrite <- Heq1, <- Heq2 in *; clear z u Heq1 Heq2. rewrite update_one_concat_l. apply binds_concat_r. apply binds_single; auto. apply notin_single; auto. destruct Hbind_l as [ Hnotin Hbind ]. destruct (eq_var_dec y z) as [ Heqz | Hneqz ]. rewrite <- Heqz in *; clear z Heqz. rewrite update_one_concat_r. rewrite update_one_single; auto. apply binds_concat_l; auto. apply notin_single; auto. apply belongs_single; auto. rewrite update_one_concat_l; [ | apply notin_single; auto ]. apply binds_concat_l; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv