proposition: Theorem all_binds_remove_inv : forall A y (E F : gen_env A), y ∉ E -> E ⊏ (F ∖ {y}) -> E ⊏ F.
proof: Proof. intros A y E F Hnotin Habind. unfold all_binds in *. intros x v Hbind. apply binds_remove_inv with y; auto. apply binds_belongs in Hbind. apply notin_belongs_neq with A E; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv