{A : Type u} →
  {inst : Ring A} →
    {relations : Module.Relations A} →
      {M : Type v} →
        {inst_1 : AddCommGroup M} →
          {inst_2 : Module A M} →
            {P : Sort u_1} →
              {var : relations.G → M} →
                {linearCombination_var_relation :
                    ∀ (r : relations.R), (Finsupp.linearCombination A var) (relations.relation r) = 0} →
                  {var' : relations.G → M} →
                    {linearCombination_var_relation' :
                        ∀ (r : relations.R), (Finsupp.linearCombination A var') (relations.relation r) = 0} →
                      { var := var, linearCombination_var_relation := linearCombination_var_relation } =
                          { var := var', linearCombination_var_relation := linearCombination_var_relation' } →
                        (var ≍ var' → P) → P