iMod and evar instantiation
See https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/acddfae5355a5e7540010c7ea6f423a892f9e887#note_17391: iMod ... as [$ ?] fails even though iMod ... as [H ?]; iFrame "H" works fine.
@jjourdan suggests it may be related to Coq lazily propagating instantiated evars, and adding a magic tactic that does the propagation in the right point of executing the iMod could help.