proposition: Theorem eq_notin : forall A x (E F : gen_env A), E ≍ F -> x ∉ E -> x ∉ F.
proof: Proof. intros A x E F Heq Hnotin. unfold eq in *. destruct Heq as [ Habind1 Habind2 ]. unfold all_binds in *. apply not_belongs_notin. intro Hin. apply belongs_binds in Hin. destruct Hin as [ v Hbind ]. apply Habind2 in Hbind. apply binds_belongs in Hbind. apply notin_belongs in Hnotin. contradiction. Qed.
imports: Utf8 Equalities CoreGenericEnv