∀ {V₁ : Type u_1} [inst : SeminormedAddCommGroup V₁] (s : AddSubgroup V₁) (x : V₁)
  (motive : x ∈ (NormedAddGroupHom.incl s).range → Prop) (x_1 : x ∈ (NormedAddGroupHom.incl s).range),
  (∀ (y : ↥s) (hy : (NormedAddGroupHom.incl s).toAddMonoidHom y = x), motive ⋯) → motive x_1