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