∀ {M : Type u_1} [inst : Add M] (S : Set (AddCon M)) (r : Setoid M) (motive : r ∈ AddCon.toSetoid '' S → Prop)
  (x : r ∈ AddCon.toSetoid '' S), (∀ (c : AddCon M) (hS : c ∈ S) (hr : c.toSetoid = r), motive ⋯) → motive x