proposition: Theorem binds_concat_inv : forall A x (v : A) (F G : gen_env A), x ∹ v ⋲ (F & G) -> x ∹ v ⋲ G ∨ (x ∉ G ∧ x ∹ v ⋲ F).
proof: Proof. induction G as [ | G y w IHG ] using env_ind; intro Hbind. rewrite concat_empty_r in *. right; split; [ apply notin_empty | ]; auto. unfold binds in *. rewrite concat_assoc in *. apply get_concat_inv in Hbind. destruct Hbind as [ [ Heq_xy Heq_wv ] | [ Hneq_xy Hget ] ]. subst. left. apply get_concat_r; auto. apply IHG in Hget. destruct Hget as [ Hget | [ Hnotin Hget ] ]. left. assert (get x (G & y ∶ w) = get x G) as Heq. apply get_concat_l; auto. rewrite Heq; auto. right. split; auto. apply notin_concat; auto. apply notin_single; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv