{P : Sort u} →
  {e : Lean.Expr} →
    {source : Lean.Meta.Grind.SplitSource} →
      {e' : Lean.Expr} →
        {source' : Lean.Meta.Grind.SplitSource} →
          Lean.Meta.Grind.SplitInfo.default e source = Lean.Meta.Grind.SplitInfo.default e' source' →
            (e = e' → source = source' → P) → P