add fixpoint lemmas for plain and absorbing
Added some lemmas about typeclass instances for fixpoints on bi_ofeO
(as opposed to least
/greatest_fixpoint
in the logic).
Added some lemmas about typeclass instances for fixpoints on bi_ofeO
(as opposed to least
/greatest_fixpoint
in the logic).