general lemma that a fixpoint is Persistent/Absorbing/Affine

Something got me thinking about when an internally defined fixpoint is persistent, and this is the result of that -- there is a general principle that looks roughly like what I expected, but it needs BiAffine and I don't quite know why. Also it would seem like this should not just work for Persistent but for all sorts of things. And I cannot quite figure out what to do with greatest fixpoints since we cannot do coinduction since there is this □ modality blocking the goal...

Is this of any use? I am also okay with just throwing it away.

Robbert has then strengthened the lemmas and also added some for Absorbing and Affine.