proposition: Lemma observing_going {E R1 R2} (eq_ : itree' E R1 -> itree' E R2 -> Prop) ot1 ot2 : going (observing eq_) ot1 ot2 <-> eq_ ot1 ot2.
proof: Proof. split; auto with itree. intros [[]]; auto. Qed.
imports: Coq(Morphisms) ITree(Core.ITreeDefinition)