fact: Definition Abel_rec_hprop (P : Type) `{IsHProp P} (a : G -> P) : Abel -> P.
imports: Basics Types Truncations.Core Cubical WildCat Colimits.Coeq Algebra.Groups.Group Algebra.AbGroups.AbelianGroup Modalities.ReflectiveSubuniverse