(motive : Lean.Meta.AbstractMVarsResult × Std.HashMap Lean.MVarId ℕ × Std.HashMap Lean.LMVarId ℕ → Sort u_1) →
  (__discr : Lean.Meta.AbstractMVarsResult × Std.HashMap Lean.MVarId ℕ × Std.HashMap Lean.LMVarId ℕ) →
    ((pat : Lean.Meta.AbstractMVarsResult) →
        (mvarIdToPatternPos : Std.HashMap Lean.MVarId ℕ) →
          (lmvarIdToPatternPos : Std.HashMap Lean.LMVarId ℕ) → motive (pat, mvarIdToPatternPos, lmvarIdToPatternPos)) →
      motive __discr