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?