doc: Codify a consistent set of rules for `#rocq_ignore` and `rocq_alias`

[markusdemedeiros]

When the port is done we should sweep the repo and decide which rocq_ignores can be upgraded to rocq_alias. At the moment, we are not consistent with this. It is not urgent, but would be nice to have the rules codified somehow.

• Should Propers be ignored, or implemented and aliased?
• Rocq syntax classes (Dist, Valid, etc) that are not present in Lean. For instances of these classes so we ignore these, or say their alias is the field of their class implementation? Should we implement the syntax classes?