proposition: Lemma rutt_clo_bind : rutt_bind_clo <3= gupaco2 (rutt_ REv RAns RR) (euttge_trans_clo RR).
proof: Proof. intros rr. gcofix CIH. intros. destruct PR. gclo; econstructor; auto_ctrans_eq. 1,2: rewrite unfold_bind; reflexivity. punfold EQV. unfold rutt_ in *. hinduction EQV before CIH; intros; pclearbot; cbn; repeat (change (ITree.subst ?k ?m) with (ITree.bind m k)). - gclo. econstructor; auto_ctrans_eq. 1,2: reflexivity. eauto with paco. - gstep. econstructor. eauto 7 with paco. - gstep. econstructor; eauto 7 with paco. intros. specialize (H0 a b H1). pclearbot. eauto 7 with paco. - gclo. econstructor; auto_ctrans_eq; cycle -1; eauto; try reflexivity. eapply eqit_Tau_l. rewrite unfold_bind. reflexivity. - gclo. econstructor; auto_ctrans_eq; cycle -1; eauto; try reflexivity. eapply eqit_Tau_l. rewrite unfold_bind. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(ITree ITreeFacts Core.Subevent Basics.HeterogeneousRelations Eq.Rutt Props.Leaf)