∀ {X : Type u_1} {M : Type u_2} [inst : PartialOrder M] (d : X → X → M) (δ : M) (x z : X)
  (motive : (x, z) ∈ SetRel.comp {x | d x.1 x.2 < δ} {x | d x.1 x.2 < δ} → Prop)
  (x_1 : (x, z) ∈ SetRel.comp {x | d x.1 x.2 < δ} {x | d x.1 x.2 < δ}),
  (∀ (y : X) (h₁ : (x, y) ∈ {x | d x.1 x.2 < δ}) (h₂ : (y, z) ∈ {x | d x.1 x.2 < δ}), motive ⋯) → motive x_1