{S : Type} {F_S : Group} {i : S -> F_S} `{IsFreeGroupOn S F_S i} {G : Group} (f g : F_S $-> G) (K : f o i == g o i) : f = g. Proof. exact (path_contr (f; K) (g; fun x => idpath))..1. Defined.
Require Import Basics Types Group Subgroup