chore: make Subrelation reducible

Author: fgdorais

src/Init/Core.lean

@@ -1330,8 +1330,8 @@ def emptyRelation {α : Sort u} (_ _ : α) : Prop :=
 `Subrelation q r` means that `q ⊆ r` or `∀ x y, q x y → r x y`.
 It is the analogue of the subset relation on relations.
 -/
-def Subrelation {α : Sort u} (q r : α → α → Prop) :=
-  ∀ {x y}, q x y → r x y
+@[reducible] def Subrelation {α : Sort u} (q r : α → α → Prop) :=
+  ∀ ⦃x y⦄, q x y → r x y
 
 /--
 The inverse image of `r : β → β → Prop` by a function `α → β` is the relation