-
Maxime Dénès authored
Previous scripts were relying on the order in which apply's HO unification performs reductions, for a goal that could be solved by reflexivity.
Previous scripts were relying on the order in which apply's HO unification performs reductions, for a goal that could be solved by reflexivity.