proposition: Theorem binds_update_inv : forall A x (v : A) (F G : gen_env A), x ∹ v ⋲ (F ::= G) -> (x ∉ G ∧ x ∹ v ⋲ F) ∨ (x ∈ F ∧ x ∹ v ⋲ G).
proof: Proof. intros A x v F G Hbind. induction G as [ | G y w IHG ] using env_ind. rewrite update_empty_r in Hbind. left; split; auto. apply notin_empty. rewrite update_concat_r in Hbind. rewrite update_update_one in Hbind. apply binds_update_one_inv in Hbind. destruct Hbind as [ Hneq | Heq ]. destruct Hneq as [ Hneq Hbind]. apply IHG in Hbind. destruct Hbind as [ HbindF | HbindG ]. destruct HbindF as [ Hnotin Hbind ]. left; split; auto. apply notin_concat; auto. apply notin_single; auto. destruct HbindG as [ HinF Hbind ]. right; split; auto. apply binds_concat_l; auto. apply notin_single; auto. destruct Heq as [ Hin [ Heq1 Heq2 ] ]; subst. right. split. apply belongs_update_inv with G; auto. apply binds_concat_r. apply binds_single; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv