HB.howto does not find instances

[Tragicus]

Here, HB.howto does not find the instances on FImFun.type (as witnessed immediately after). Besides, the second Check fails for unknown reasons, but this might be unrelated to HB.