RFC: Make `Subrelation` reducible

Proposal

Make Subrelation reducible in Init.Core so that it becomes a drop-in replacement for its spelled-out definition.

Impact

Currently, Subrelation is usually spelled out when it occurs as a hypothesis in Batteries and Mathlib. Though not overwhelmingly common, there are several instances of this. For example, this came up in a PR discussion in Batteries today:

theorem IsChain.imp (H : ∀ ⦃a b⦄, R a b → S a b) {l : List α} (p : IsChain R l) : IsChain S l := ...

Notice the non-descriptive name imp, which could be easily improved with a name that mentions subrelation.

Having a reducible Subrelation would also help standardize the exact type of this kind of hypothesis.

The proposed change appears to be harmless: the tentative PR #10464 does not cause any breaks in Lean, Batteries, or Mathlib.

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

The entry point named is Init.Core; inspect the definition of Subrelation there and compare the proposed change with tentative PR #10464. Confirm done by checking that Lean, Batteries, and Mathlib remain unbroken, as the issue reports.