proposition: Theorem binds_all_remove_inv : forall A x ys (v : A) (E : gen_env A), ¬ List.In x ys -> x ∹ v ⋲ (E ∖ ys) -> x ∹ v ⋲ E.
proof: Proof. induction ys as [ | y ys ]; intros v E Hnotin Hbind; simpl in *; auto. rewrite all_remove_nil in Hbind; auto. rewrite all_remove_remove in Hbind. assert (y <> x ∧ ¬ List.In x ys) as Hneq. split; auto. destruct Hneq. apply binds_remove_inv with y; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv