{P : Sort u} →
  {elimInfo : Lean.Elab.Term.ElabElimInfo} →
    {expectedType : Lean.Expr} →
      {elimInfo' : Lean.Elab.Term.ElabElimInfo} →
        {expectedType' : Lean.Expr} →
          { elimInfo := elimInfo, expectedType := expectedType } =
              { elimInfo := elimInfo', expectedType := expectedType' } →
            (elimInfo = elimInfo' → expectedType = expectedType' → P) → P