∀ {R : Type u_1} [inst : Add R] {c : R} (motive : IsAddLeftRegular c ∧ IsAddRightRegular c → Prop)
  (x : IsAddLeftRegular c ∧ IsAddRightRegular c),
  (∀ (h1 : IsAddLeftRegular c) (h2 : IsAddRightRegular c), motive ⋯) → motive x