Remove useless implicit annotation on binder

Fixes a new warning on Coq 8.12+alpha when implicit annotations are used in positions where they are ignored.