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