proposition: Theorem eq_all_notin : forall A xs (E F : gen_env A), E ≍ F -> xs ⊄ E -> xs ⊄ F.
proof: Proof. intros A xs E F Heq Hnotin. apply all_notin_def. intros. apply eq_notin with E; auto. apply all_notin_def_inv with xs; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv