proposition: Theorem all_binds_all_remove_inv : forall A ys (E F : gen_env A), ys ⊄ E -> E ⊏ (F ∖ ys) -> E ⊏ F.
proof: Proof. intros A ys E F Hnotin Habind. unfold all_binds in *. intros x v Hbind. apply binds_all_remove_inv with ys; auto. apply binds_belongs in Hbind. apply all_notin_belongs_neq with A E; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv