proposition: Lemma sutt_trace_incl : forall {E R} (t1 t2 : itree E R), sutt eq t1 t2 -> trace_incl t1 t2.
proof: Proof. red. intros. red in H0. remember (observe t1). generalize dependent t1. generalize dependent t2. induction H0; intros; try solve [constructor]. - punfold H. rewrite <- Heqi in H. remember (RetF _). remember (observe t2). generalize dependent t2. induction H; intros; try inv Heqi0; red; rewrite <- Heqi1; constructor. eapply IHsuttF; eauto. - apply IHis_traceF with (t1:=t); auto. apply sutt_inv_tau_left. red. red in H. rewrite <- Heqi in H. auto. - punfold H. rewrite <- Heqi in H. remember (VisF _ _). remember (observe t2). generalize dependent t2. induction H; intros; try discriminate. + inv_Vis. subst. red. rewrite <- Heqi1. constructor. + red. rewrite <- Heqi1. constructor. eapply IHsuttF; eauto. - punfold H. rewrite <- Heqi in H. remember (VisF _ _). remember (observe t2). generalize dependent t2. induction H; intros; try discriminate. + inv_Vis. pclearbot. subst. red. rewrite <- Heqi1. constructor. eapply IHis_traceF; auto with itree. + red. rewrite <- Heqi1. constructor. apply IHsuttF; auto. Qed.
imports: Paco(paco) ITree(Basics.Utils Axioms Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.SimUpToTaus Eq.Shallow Eq.Paco2)