YaZko
commented
2 years ago This has been done. Since the coinduction package does not support this very well currently, we redefine locally tactics to additionally take care of the unfolding and refolding of the definitions.
Be sure to import Eq.v to get the corresponding surface tactics.
Similar support for wbisim is not quite there yet at the moment but will be easy to add when relevant.
Following the [coinduction] library style, most greatest fixed-points are simple notations rather than definitions. This creates a lot of pain-points, notably when their implicit parameters need to be provided explicitly.
We want to move to definitions at some point to clean this up, but it might be a little delicate, the unifications problems that result from applying the very generic lemmas from the coinduction library being quite brittle.