proposition: Lemma itree_eta_ (t : itree E R) : t ≅ go (_observe t).
proof: Proof. apply observing_sub_eqit. econstructor. reflexivity. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)