proposition: Theorem binds_remove_inv : forall A x y (v : A) (E : gen_env A), x <> y -> x ∹ v ⋲ (E ∖ {y}) -> x ∹ v ⋲ E.
proof: Proof. intros A x y v E Hneq Hbind. induction E as [ | E z w IHE ] using env_ind. rewrite remove_empty in Hbind. apply binds_empty in Hbind. inversion Hbind. destruct (eq_keys_dec y z); subst. rewrite remove_belongs_concat_r in Hbind. rewrite remove_single_eq in Hbind; auto. rewrite concat_empty_r in Hbind. apply binds_concat_l; auto. apply notin_single; auto. apply belongs_single; auto. destruct (eq_keys_dec x z); subst. rewrite remove_belongs_concat_l in Hbind. apply binds_concat_inv in Hbind. destruct Hbind as [ Hbind | [ Hnotin Hbind ] ]. apply binds_concat_r; auto. apply notin_single_inv in Hnotin. elim Hnotin; auto. apply notin_single; auto. rewrite remove_belongs_concat_l in Hbind. apply binds_concat_inv in Hbind. destruct Hbind as [ Hbind | [ Hnotin Hbind ] ]. apply binds_single_inv in Hbind. destruct Hbind; contradiction. apply binds_concat_l; auto. apply notin_single; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv