∀ {A : Type u} {inst : Ring A} {relations : Module.Relations A} {M : Type v} {inst_1 : AddCommGroup M}
  {inst_2 : Module A M} {solution : relations.Solution M}
  {desc : {N : Type w'} → [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → relations.Solution N → M →ₗ[A] N}
  {postcomp_desc :
    ∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N),
      solution.postcomp (desc s) = s}
  {postcomp_injective :
    ∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] {f f' : M →ₗ[A] N},
      solution.postcomp f = solution.postcomp f' → f = f'}
  {desc_1 : {N : Type w'} → [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → relations.Solution N → M →ₗ[A] N}
  {postcomp_desc_1 :
    ∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N),
      solution.postcomp (desc_1 s) = s}
  {postcomp_injective_1 :
    ∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] {f f' : M →ₗ[A] N},
      solution.postcomp f = solution.postcomp f' → f = f'},
  { desc := desc, postcomp_desc := postcomp_desc, postcomp_injective := postcomp_injective } =
      { desc := desc_1, postcomp_desc := postcomp_desc_1, postcomp_injective := postcomp_injective_1 } →
    desc = desc_1