Define fixpoint predicates

The following discussion from !319 (merged) should be addressed:

• @bbb started a discussion: (+1 comment)

  Should we make these predicates proper definitions (nat -> Prop)?

  • aRSA_fixpoint R
  • aRTA_fixpoint R
  • bw_fixpoint L

  Looks kinda neat, I think.

  We keep referring to these, also in discussion (e.g., w/ Matteo), perhaps named definitions would help?