Interaction between clausal simplifier and spurious hypothesis

[Bronsa]

Whenever you have an explicit equality hypothesis between a variable and a non-variable term that doesn't contain it, that leads to an 'explicit substitution' that eliminates the variable - that's so that we have minimal hypotheses before an induction.
In certain cases, this can lead to Imandra removing "manual" destructor elimination, and thus failing to automatically prove a goal by induction.

A key takeaway is, if you have a goal that is going to be proved by induction, always try to make it as strong as possible. As much as possible, you never want to have spurious hypotheses in something you're proving by induction, because then your inductive hypotheses are weaker.