proposition: Theorem binds_update_one_inv : forall A x y (v w : A) (F : gen_env A), x ∹ v ⋲ (F [y <- w]) -> (x <> y ∧ x ∹ v ⋲ F) ∨ (x ∈ F ∧ x = y ∧ v = w).
proof: Proof. intros A x y v w F Hbind. induction F as [ | F z u IHF ] using env_ind. rewrite update_one_empty in Hbind. apply binds_empty in Hbind. inversion Hbind. destruct (eq_var_dec y z) as [ Heqz | Hneqz ]; destruct (eq_var_dec x y) as [ Heqy | Hneqy ]; subst. Focus. rewrite update_one_concat_r in Hbind; [ | apply belongs_single; auto ]. rewrite update_one_single in Hbind; auto. apply binds_concat_inv in Hbind. destruct Hbind as [ Hin | Hnotin ]. apply binds_single_inv in Hin. destruct Hin; subst. right. split; auto. apply belongs_concat_r. apply belongs_single; auto. destruct Hnotin as [ Hnotin _ ]. apply notin_single_inv in Hnotin. elim Hnotin; auto. Focus. rewrite update_one_concat_r in Hbind; [ | apply belongs_single; auto ]. rewrite update_one_single in Hbind; auto. apply binds_concat_inv in Hbind. destruct Hbind as [ Hin | Hnotin ]. apply binds_single_inv in Hin. destruct Hin; contradiction. left. split; auto. apply binds_concat_l. destruct Hnotin; auto. apply notin_single; auto. Focus. rewrite update_one_concat_l in Hbind; [ | apply notin_single; auto ]. apply binds_concat_inv in Hbind. destruct Hbind as [ Hin | Hnotin ]. apply binds_single_inv in Hin. destruct Hin; contradiction. destruct Hnotin as [ Hnotin Hbind ]. apply IHF in Hbind. destruct Hbind as [ Hneq | Heq ]. destruct Hneq as [ Hneq _ ]. elim Hneq; auto. destruct Heq as [ HinF Heqs ]. destruct Heqs. right. split; auto. apply belongs_concat_l; auto. destruct (eq_var_dec x z) as [ Heq | Hneq ]; subst. rewrite update_one_concat_l in Hbind; [ | apply notin_single; auto ]. apply binds_concat_inv in Hbind. destruct Hbind as [ Hin | Hnotin ]. apply binds_single_inv in Hin. destruct Hin; subst. left. split; auto. apply binds_concat_r. apply binds_single; auto. destruct Hnotin as [ Hnotin _ ]. apply notin_single_inv in Hnotin. elim Hnotin; auto. rewrite update_one_concat_l in Hbind; [ | apply notin_single; auto ]. apply binds_concat_inv in Hbind. destruct Hbind as [ Hin | Hnotin ]. apply binds_single_inv in Hin. destruct Hin; contradiction. destruct Hnotin as [ Hnotin Hbind ]. apply IHF in Hbind. destruct Hbind as [ Hneq2 | Heq ]; [ | destruct Heq as [ _ Heq ]; destruct Heq; contradiction ]. destruct Hneq2. left. split; auto. apply binds_concat_l; [ | apply notin_single; auto ]; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv