∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] {c : RingCon M} (f : M →+* N)
  {x y : M} (motive : (∃ a b, c a b ∧ f a = f x ∧ f b = f y) → Prop) (x_1 : ∃ a b, c a b ∧ f a = f x ∧ f b = f y),
  (∀ (a b : M) (h₁ : c a b) (h₂ : f a = f x) (h₃ : f b = f y), motive ⋯) → motive x_1