Hi, I am trying to prove a goal with ML. At first it did not work at all due to 'pending sort hypothesis'. After reading about that I removed all unnecessary forall-bound variables and the goal is proven as expected.

However if I add a definition for part of the body of the goal using `Local_Theory.define_internal`

and try to prove that, i get 'pending sort hypothesis' again, even though the goal has no foralls at all.

Does anyone know why this is happening?

Last updated: Dec 07 2023 at 16:21 UTC