proposition: Lemma trace_incl_sutt : forall {E R} (t1 t2 : itree E R), trace_incl t1 t2 -> sutt eq t1 t2.
proof: Proof. intros E R. pcofix CIH. pstep. intros t1 t2 Hincl. unfold trace_incl in *. unfold is_trace in *. destruct (observe t1). - assert (H : is_traceF (RetF r0 : itreeF E R (itree E R)) (TRet r0)) by constructor. apply Hincl in H. clear Hincl. destruct (observe t2); inv H. + constructor. auto. + constructor. remember (observe t). remember (TRet _). generalize dependent t. induction H1; intros; try inv Heqt0; auto with itree. constructor. eapply IHis_traceF; eauto. - constructor. right. apply CIH. intros. apply Hincl. constructor. auto. - assert (H: is_traceF (VisF e k) (TEventEnd e)) by constructor. apply Hincl in H. destruct (observe t2); inv H. + constructor. assert (forall tr, is_traceF (VisF e k) tr -> is_traceF (observe t) tr). { intros. rewrite is_traceF_tau. apply Hincl; auto. } clear Hincl. rename H into Hincl. remember (observe t). remember (TEventEnd _). generalize dependent t. induction H1; intros; try discriminate. * constructor. eapply IHis_traceF; eauto. intros. rewrite is_traceF_tau. apply Hincl; auto. * apply eq_trace_inv in Heqt0; destruct Heqt0 as [<- <-]. subst. constructor. intro. right. apply CIH. intros. assert (is_traceF (VisF e k) (TEventResponse e x tr)) by (constructor; auto). apply Hincl in H1. inv H1. ddestruction. auto. + ddestruction. constructor. intro. right. apply CIH. intros. assert (is_traceF (VisF e0 k) (TEventResponse e0 x tr)) by (constructor; auto). apply Hincl in H0. inv H0. ddestruction; auto. Qed.
imports: Paco(paco) ITree(Basics.Utils Axioms Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.SimUpToTaus Eq.Shallow Eq.Paco2)