Stdpp has support for easily constructing reflexive transitive closures using rtc of https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/relations.v .
It seems fruitful to have a similar library for functions into bi.
Stdpp has support for easily constructing reflexive transitive closures using rtc of https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/relations.v .
It seems fruitful to have a similar library for functions into bi.