The rules for module instantiation specify that declarative element segments are dropped during instantiation [1]:

runelem𝑖({type et, init ref 𝑛, mode declarative}) =
(elem.drop 𝑖)

But the prose only has a rule for active element segments:

For each element segment elem𝑖 in module.elems whose mode is of the form
active {table tableidx 𝑖, offset einstr *
𝑖 end}, do:
  ...

I think we need an extension to the prose to mention that declarative segments are dropped during instantiation.

[1] https://webassembly.github.io/spec/core/exec/modules.html#instantiation