It seems some lemmas are incompatible with 8.15.1, or something is wrong on my end.
The problems are in HahnMinPath and HahnWf.
the problem in HahnWf seems to be related to a mismatch between the internal name of the binder (y) and what is shown on screen (y0). It can be fixed like this:
rename y into y'. (* not necessary, but makes sure that the names stay the same *)
apply In_split in IN; desf.
eapply H with (y := l1 ++ l2); ins. (* was y0:= *)
by rewrite !app_length; simpl; lia.
However it's strange that the names are not the same and could point to the problem being in my installation.
It seems some lemmas are incompatible with 8.15.1, or something is wrong on my end.
The problems are in HahnMinPath and HahnWf.
the problem in HahnWf seems to be related to a mismatch between the internal name of the binder (y) and what is shown on screen (y0). It can be fixed like this:
However it's strange that the names are not the same and could point to the problem being in my installation.