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