∀ {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SizeOf R] [inst_2 : SizeOf M] (carrier : Set M)
  (smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier),
  sizeOf { carrier := carrier, smul_mem' := smul_mem' } = 1