{A B : Group} (f : A $-> B) : A $-> grp_image f. Proof. snrapply Build_GroupHomomorphism. { intro x. exists (f x). srapply tr. exists x. reflexivity. } cbn. grp_auto. Defined.
Require Import Basics Types. Require Import Truncations.Core. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. Require Import WildCat.Core. Require Import HSet.