n m (f : FinSeq m (FreeGroup (Fin n))) : GroupPresentation. Proof. snrapply Build_GroupPresentation. - exact (Fin n). - exact (Fin m). - exact f. Defined.
Require Import Basics Types. Require Import Truncations.Core. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.FreeGroup. Require Import Algebra.Groups.GroupCoeq. Require Import Spaces.Finite Spaces.List.Core. Require Import WildCat.