proposition: Theorem all_binds_single_push_inv : forall A x y (v w : A) (E : gen_env A), (x ∶ v) ⊏ (E & (y ∶ w)) -> (x = y ∧ v = w) ∨ (x <> y ∧ (x ∶ v) ⊏ E).
proof: Proof. intros A x y v w E Habind. apply all_binds_binds in Habind. apply binds_concat_inv in Habind. destruct Habind as [ Hbind | [ Hnotin Hbind ] ]. apply binds_single_inv in Hbind. left; auto. apply notin_single_inv in Hnotin. apply binds_all_binds in Hbind. right; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv