Support `PartialOrd` and other generated things

[W95Psp]

For a bunch of "standard" derived core traits, we just ignore generated code.

• PartialOrd, Ord: straightforward, we might want lemmas saying that if x <= y and x >= y, then x == y, but this might not always be true (note: Ord vs PartialOrd, and is == Rust equality or theorem prover equality?)
• PartialEq, Eq: more complicated. It's perfectly fine to implement Eq and PartialEq to reflect equality on a partial view of a value.
• Debug: should be fairly easy
• Copy: implement as identity, it's only a marker-trait
• Clone: I think we still want to model clones as copies. A clone that is doing something more than cloning sub-values usually means it's doing a side effect (e.g. Rc).

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.