With Coq master, we otherwise fail to infer instances with subG_savedAnythingΣ, which leads to goals like
looking for (subG
(@savedAnythingΣ (@ofe_funCF val (fun _ : val => laterCF idCF))
?cFunctorContractive0) Σ)