proposition: Theorem TorsorIso_rect' {G:gr} {X : Torsor G} (P : ∏ Y : Torsor G, ActionIso X Y -> Type) : P X (idActionIso X) -> ∏ (Y : Torsor G) (f:ActionIso X Y), P Y f.
proof: Proof. intros p ? ?. torsor_induction f q. induction q. exact p. 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