Fixes a bug from !488 (merged)
The code was inferring an implicit in some complicated way that works on 8.11+. Apparently ; by eauto in later versions is like ; eauto; done (this solves goals 1 and 3, then 2) while in Coq 8.10 it failed because eauto; done fails in the second goal.
CC @robbertkrebbers and @jung