proposition: Lemma is_traceF_tau : forall {E R} (t : itree E R) tr, is_traceF (observe t) tr <-> is_traceF (TauF t) tr.
proof: Proof. intros. split; intros. - constructor. remember (observe t). generalize dependent t. induction H; intros; subst; constructor; eapply IHis_traceF; auto. - inversion H; subst; try constructor; auto. Qed.
imports: Paco(paco) ITree(Basics.Utils Axioms Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.SimUpToTaus Eq.Shallow Eq.Paco2)