What's going on in this proof is that
simpl is unfolding both
decode, even though
decode is marked
simpl never. This is a bug in Coq and std++ should not rely on it.
Alternate take on https://gitlab.inria.fr/bertot/stdpp/-/commit/895121f919c6f1332f41f658ce7f850e391eb49e, which is used as an overlay in Coq for https://github.com/coq/coq/pull/13448.