∀ {G : Type u_1} [inst : AddGroup G] {k : Set G} {p : (g : G) → g ∈ AddSubgroup.closure k → Prop},
  (∀ (x : G) (hx : x ∈ k), p x ⋯) →
    p 0 ⋯ →
      (∀ (x y : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k), p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x : G) (hx : x ∈ AddSubgroup.closure k), p x hx → p (-x) ⋯) →
          ∀ {x : G} (hx : x ∈ AddSubgroup.closure k), p x hx