This removes the lemma that is causing the issue. I'm not entirely sure why it works here but no in the coq CI. But it's not a very important lemma so we can figure it out later.
Checklist
[x] added corresponding entries in CHANGELOG_UNRELEASED.md
[x] added corresponding documentation in the headers
proux01
commented
4 days ago
Fixes #1333
This removes the lemma that is causing the issue. I'm not entirely sure why it works here but no in the coq CI. But it's not a very important lemma so we can figure it out later.
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Reminder to reviewers