Assert failure while using destruct_rec
The assert false in
src/core/trans.ml at line 183 can be violated.
I have encountered the error in the middle of a larger proof so it is a bit difficult to isolate a MWE. But please let me know if you need one or want to have a look at the proof, or if you have already an idea about the culprit.