proposition: Theorem trace_incl_iff_sutt : forall {E R} (t1 t2 : itree E R), sutt eq t1 t2 <-> trace_incl t1 t2.
proof: Proof. split. - apply sutt_trace_incl. - apply trace_incl_sutt. Qed.
imports: Paco(paco) ITree(Basics.Utils Axioms Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.SimUpToTaus Eq.Shallow Eq.Paco2)