(motive : Array Lean.FVarId × Lean.MVarId → Sort u_1) →
  (__discr : Array Lean.FVarId × Lean.MVarId) →
    ((fvarIds : Array Lean.FVarId) → (goal : Lean.MVarId) → motive (fvarIds, goal)) → motive __discr