https://github.com/DeepSpec/InteractionTrees/blob/master/extra/IForest.v#L70 Trick: define a coinductive relation `relbind : itree E A -> (A -> itree E B -> Prop) -> itree E B -> Prop`
https://github.com/DeepSpec/InteractionTrees/blob/master/extra/IForest.v#L70
Trick: define a coinductive relation
relbind : itree E A -> (A -> itree E B -> Prop) -> itree E B -> Prop