proposition: Lemma eqit_Leaf_clo_bind (RS : R -> S -> Prop) b1 b2 vclo (MON: monotone2 vclo) (CMP: compose (eqitC RS b1 b2) vclo <3= compose vclo (eqitC RS b1 b2)) (ID: id <3= vclo): eqit_Leaf_bind_clo b1 b2 <3= gupaco2 (eqit_ RS b1 b2 vclo) (eqitC RS b1 b2).
proof: Proof. gcofix CIH. intros. destruct PR. guclo eqit_clo_trans. econstructor; auto_ctrans_eq; try (rewrite (itree_eta (x <- _;; _ x)), unfold_bind; reflexivity). punfold EQV. unfold_eqit. genobs t1 ot1. genobs t2 ot2. hinduction EQV before CIH; intros; pclearbot. - guclo eqit_clo_trans. econstructor; auto_ctrans_eq; try (rewrite <- !itree_eta; reflexivity). gbase; cbn. apply REL0; auto with itree. - gstep. econstructor. gbase. apply CIH. econstructor; eauto with itree. - gstep. econstructor. intros; apply ID; unfold id. gbase. apply CIH. econstructor; eauto with itree. - destruct b1; try discriminate. guclo eqit_clo_trans. econstructor. 3:{ eapply IHEQV; eauto with itree. } 3,4:auto_ctrans_eq. 2: reflexivity. eapply eqit_Tau_l. rewrite unfold_bind, <-itree_eta. reflexivity. - destruct b2; try discriminate. guclo eqit_clo_trans. econstructor; auto_ctrans_eq; eauto with itree; try reflexivity. eapply eqit_Tau_l. rewrite unfold_bind, <-itree_eta. reflexivity. Qed.
imports: ITree(Basics.Utils Basics.HeterogeneousRelations ITree Eq.Shallow Eq.Eqit Interp.InterpFacts Events.State Events.StateFacts Props.HasPost) Paco(paco) Coq(Morphisms Basics Program.Equality)