proposition: Theorem all_binds_all_remove_compat : forall A xs (E F : gen_env A), ok E -> ok F -> E ⊏ F -> E ∖ xs ⊏ F ∖ xs.
proof: Proof. induction xs as [ | x xs IHxs ]; intros E F Hok1 Hok2 Habind; simpl in *; auto. rewrite ?all_remove_nil; auto. assert (E ∖ {x} ⊏ F ∖ {x}) by (apply all_binds_remove_compat; auto). rewrite ?all_remove_remove. apply IHxs; auto; apply ok_remove; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv