Coq: more solving support for boolean predicates

Mostly from making the aarch64 model compile again
- switch order some arithmetic lemmas
- move list membership rewrites alongside other comparisons to enable more
  rewriting
- copy hypotheses used in other types/definitions so that they can be
  rewritten
- lift boolean existentials out of implications in hypotheses so they can
  be used as witnesses without proving the condition
- add negation to solve_bool_with_Z
- add some new bool solving for goals from and_boolMP/or_boolMP

0 files changed, 0 insertions, 0 deletions