proposition: Lemma eutt_post_bind : forall E R1 R2 RR S1 S2 SS Q1 Q2 (t1 : itree E S1) (k1: S1 -> itree E R1) (t2 : itree E S2) (k2 : S2 -> itree E R2), t1 ⤳ Q1 -> t2 ⤳ Q2 -> eutt SS t1 t2 -> (forall u1 u2, SS u1 u2 -> Q1 u1 -> Q2 u2 -> eutt RR (k1 u1) (k2 u2)) -> eutt RR (ITree.bind t1 k1) (ITree.bind t2 k2).
proof: Proof. intros * POST1 POST2 EQ KEQ. apply eutt_clo_bind with (UU := fun x y => SS x y /\ Q1 x /\ Q2 y). 2: intros ? ? (? & ? & ?); apply KEQ; auto. clear KEQ. apply has_post_post_strong in POST1. apply has_post_post_strong in POST2. pose proof eqit_trans _ _ _ _ _ _ _ POST1 EQ as EQ1. pose proof eqit_trans _ _ _ _ _ _ _ EQ1 POST2 as EQ2. clear -EQ2. eapply eutt_equiv; eauto. split. - intros ? ? (? & ? & ?); do 2 econstructor; eauto. - intros ? ? ?. inv H. inv REL1. destruct REL2 as [-> ?], REL0 as [<- ?]; eauto. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Basics.Utils ITree Eq.Eqit Basics.HeterogeneousRelations Interp.TranslateFacts)