Universe inconsistency with ITree.Events.StateFacts

[elefthei]

We tried to solve this with @euisuny and @YaZko but I had to leave. Making a note here that

From ITree Require Import
     Events.StateFacts.

From CTree Require Import
     Bisim.

Gives a universe inconsistency error

Error: Universe inconsistency. Cannot enforce Coq.Relations.Relation_Definitions.1 <= RelationAlgebra.monoid.1 because
RelationAlgebra.monoid.1 <= Coq.Lists.List.1 <= MonadFix.MonadFix.u0 < Coq.Relations.Relation_Definitions.1.

[YaZko]

Yes, thanks for recording this!

If I am not mistaken, Bisim is only a vessel for the issue, I think (but am not sure) that the problem has to do with the use of the RelationAlgebra library that we make in Trans.v to work in the Kleene Algebra against a model where the equality is equ.

Note that this is the exact same issue as in examples/Yield/Lang.v where we shamefully killed universe checks for now rather than dealing with it.