proposition: Lemma eutt_conj {E} {R S} {RS RS'} : forall (t : itree E R) (s : itree E S), eutt RS t s -> eutt RS' t s -> eutt (RS /2\ RS') t s.
proof: Proof. repeat red. einit. ecofix CIH. intros * EQ EQ'. rewrite itree_eta, (itree_eta s). punfold EQ; punfold EQ'; red in EQ; red in EQ'. genobs t ot; genobs s os. hinduction EQ before CIHH; subst; intros; pclearbot; simpl. - estep; split; auto. inv EQ'; auto. - estep; ebase; right; eapply CIHL; eauto. rewrite <- tau_eutt. rewrite <- (tau_eutt m2); auto with itree. - assert (EE := eqitF_inv_VisF _ _ _ _ _ EQ'); pclearbot. eapply euttG_vis; ebase; left; apply CIHH; auto with itree. - eapply fold_eqitF in EQ'; eauto. assert (t ≈ Tau t1) by (rewrite itree_eta, <- Heqot; reflexivity). rewrite H in EQ'. apply eqit_inv_Tau_l in EQ'. subst; specialize (IHEQ _ _ eq_refl eq_refl). punfold EQ'; red in EQ'. specialize (IHEQ EQ'). rewrite eqit_Tau_l; [|reflexivity]. rewrite (itree_eta t1). eapply IHEQ. - subst; cbn. rewrite tau_euttge. rewrite (itree_eta t2); eapply IHEQ; eauto. eapply fold_eqitF in EQ'; eauto. assert (s ≈ Tau t2). rewrite (itree_eta s), <- Heqos; reflexivity. rewrite tau_eutt in H. assert (eutt RS' t t2). rewrite <- H; auto. punfold H0. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)