fact: Record observing {E R1 R2} (eq_ : itree' E R1 -> itree' E R2 -> Prop) (t1 : itree E R1) (t2 : itree E R2) : Prop := observing_intros { observing_observe : eq_ (observe t1) (observe t2) }.
imports: Coq(Morphisms) ITree(Core.ITreeDefinition)