proposition: Theorem all_binds_remove_compat : forall A x (E F : gen_env A), ok E -> ok F -> E ⊏ F -> E ∖ {x} ⊏ F ∖ {x}.
proof: Proof. intros A x E F Hok1 Hok2 Habind. unfold all_binds in *. intros y v Hbind. assert (y <> x) by (apply belongs_remove_inv with A E; auto; apply binds_belongs with v; auto). apply binds_remove; auto. apply Habind. apply binds_remove_inv with x; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv