Merged requested to merge tchajed/iris-coq:fix-mr-488 into master
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