proposition: Lemma eqit_clo_bind b1 b2 vclo (MON: monotone2 vclo) (CMP: compose (eqitC RR b1 b2) vclo <3= compose vclo (eqitC RR b1 b2)) (ID: id <3= vclo): eqit_bind_clo b1 b2 <3= gupaco2 (eqit_ RR b1 b2 vclo) (eqitC RR b1 b2).
proof: Proof. intros rr. pcofix CIH. intros. destruct PR. guclo eqit_clo_trans. econstructor; auto_ctrans_eq. 1,2: rewrite unfold_bind; reflexivity. punfold EQV. unfold_eqit. hinduction EQV before CIH; intros; pclearbot; cbn; repeat (change (ITree.subst ?k ?m) with (ITree.bind m k)). - guclo eqit_clo_trans. econstructor; auto_ctrans_eq. 1,2: reflexivity. eauto with paco. - gstep. econstructor. eauto 7 with paco itree. - gstep. econstructor. intros. red in CMP. unfold id in ID. apply ID. eauto 7 with paco itree. - destruct b1; try discriminate. guclo eqit_clo_trans. econstructor; auto_ctrans_eq; eauto; try reflexivity. eapply eqit_Tau_l. rewrite unfold_bind. reflexivity. - destruct b2; try discriminate. guclo eqit_clo_trans. econstructor; auto_ctrans_eq; eauto; try reflexivity. eapply eqit_Tau_l. rewrite unfold_bind. reflexivity. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)