proposition: Theorem eq_all_remove : forall A xs (E F : gen_env A), ok E -> ok F -> E ≍ F -> E ∖ xs ≍ F ∖ xs.
proof: Proof. intros A xs E F Hok1 Hok2 Heq. unfold eq in *. destruct Heq. split; apply all_binds_all_remove_compat; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv