proposition: Theorem binds_update_one_eq : forall A x y (v w : A) (F : gen_env A), x ∈ F -> x = y -> v = w -> x ∹ v ⋲ (F [y <- w]).
proof: Proof. intros A x y v w F Hbelongs Heq_xy Heq_vw. rewrite <- Heq_xy, <- Heq_vw in *; clear y w Heq_xy Heq_vw. induction F as [ | F z u ] using env_ind. apply belongs_empty in Hbelongs. inversion Hbelongs. destruct (eq_var_dec x z) as [ Heq | Hneq ]. rewrite <- Heq in *; clear z Heq. rewrite update_one_concat_r; [ | apply belongs_single; auto ]. rewrite update_one_single; auto. apply binds_concat_r. apply binds_single; auto. apply belongs_concat_inv in Hbelongs. destruct Hbelongs as [ HinF | Hinz]. rewrite update_one_concat_l; [ | apply notin_single; auto ]. apply binds_concat_l; [ | apply notin_single; auto ]; auto. apply belongs_single_inv in Hinz. contradiction. Qed.
imports: Utf8 Equalities CoreGenericEnv