proposition: Proposition grp_iso_cxfib_beta {A B C : Group} {i : A $-> B} {f : B $-> C} `{IsEmbedding i} (ex : IsExact (Tr (-1)) i f) : i $o (grp_iso_inverse (grp_iso_cxfib ex)) $== subgroup_incl (grp_kernel f).
proof: Proof. rapply equiv_ind. 1: exact (isequiv_cxfib ex). intro x. exact (ap (fun y => i y) (eissect _ x)). Defined.
imports: Basics Types Truncations.Core WildCat.Core Pointed Groups.Group Groups.Subgroup Groups.Kernel Homotopy.ExactSequence Modalities.Identity