proposition: Theorem eq_belongs : forall A x (E F : gen_env A), E ≍ F -> x ∈ E -> x ∈ F.
proof: Proof. intros A x E F Heq Hin. unfold eq in *. destruct Heq as [ Habind1 Habind2 ]. unfold all_binds in *. apply belongs_binds in Hin. destruct Hin as [ v Hbind ]. apply Habind1 in Hbind. apply binds_belongs with v; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv