∀ {G : Type u_1} [inst : AddGroup G] {s t : AddSubgroup G} {x : G} (motive : (∃ y ∈ t, ∃ z ∈ s, y + z = x) → Prop)
  (x_1 : ∃ y ∈ t, ∃ z ∈ s, y + z = x),
  (∀ (y : G) (hy : y ∈ t) (z : G) (hz : z ∈ s) (hp : y + z = x), motive ⋯) → motive x_1