(motive : List Lean.MVarId × List Lean.MVarId × List Lean.MVarId → Sort u_1) →
  (__discr : List Lean.MVarId × List Lean.MVarId × List Lean.MVarId) →
    ((egoals acc insts : List Lean.MVarId) → motive (egoals, acc, insts)) → motive __discr