∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {motive : (a a_1 : M) → ConGen.Rel r a a_1 → Prop} {x y z : M}
  (a : ConGen.Rel r x y) (a_1 : ConGen.Rel r y z),
  ConGen.Rel.below a → motive x y a → ConGen.Rel.below a_1 → motive y z a_1 → ConGen.Rel.below ⋯