proposition: Theorem eq_map : forall A B (f : A -> B) (E F : gen_env A), E ≍ F -> map f E ≍ map f F.
proof: Proof. intros A B f E F Heq. unfold eq in *. destruct Heq. split; apply all_binds_map; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv