∀ {N : Type u_1} [inst : AddZeroClass N] {M : Type u_2} [inst_1 : AddZeroClass M] (s : AddSubmonoid N) (p : M × N)
  (motive : p ∈ ⊥.prod s → Prop) (x : p ∈ ⊥.prod s), (∀ (hp1 : p.1 ∈ ↑⊥) (hps : p.2 ∈ ↑s), motive ⋯) → motive x