proposition: Lemma underlyingAction_incl {G:gr} : isincl (underlyingAction : Torsor G -> Action G).
proof: Proof. intros. refine (isinclpr1 _ _); intro X. apply is_torsor_isaprop. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.Tactics UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Combinatorics.OrderedSets