This PR contains a small modification of @stefaniatadama 's code in #1129 . There were some problems with showing that containers are closed under greatest fixed points due to issues with coinduction and the termination checker which forced us to include additional set assumptions. This PR removes those assumptions by introducing a bit of nasty path algebra instead:-)
This PR contains a small modification of @stefaniatadama 's code in #1129 . There were some problems with showing that containers are closed under greatest fixed points due to issues with coinduction and the termination checker which forced us to include additional set assumptions. This PR removes those assumptions by introducing a bit of nasty path algebra instead:-)