Describe the improvement you'd like to request

According to this comment we return the HierarchyNotRespected error in some cases where we could soundly type an expression as False. This error was introduced (IIRC) to avoid having to update the Dafny type soundness proof.

Now that we've switched to using Lean, and tweaked the validation property being tested, I wonder if we could remove this error variant.

Describe alternatives you've considered

No response

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this internal improvement
• ⚠️ This feature might incur a breaking change