proposition: Lemma interp_mrec_rutt (R1 R2 : Type) (RR : R1 -> R2 -> Prop) : forall (t1 : itree (D1 +' E1) R1) (t2 : itree (D2 +' E2) R2), rutt (sum_prerel RPreInv RPre) (sum_postrel RPostInv RPost) RR t1 t2 -> rutt RPre RPost RR (interp_mrec bodies1 t1) (interp_mrec bodies2 t2).
proof: Proof. ginit. gcofix CIH. intros t1 t2 Ht12. punfold Ht12. red in Ht12. remember (observe t1) as ot1. remember (observe t2) as ot2. hinduction Ht12 before r; intros. - apply simpobs in Heqot1, Heqot2. rewrite Heqot1, Heqot2. gstep. red. cbn. constructor. auto. - apply simpobs in Heqot1, Heqot2. rewrite Heqot1, Heqot2. repeat rewrite unfold_interp_mrec. cbn. gstep. constructor. pclearbot. gfinal. eauto. - apply simpobs in Heqot1, Heqot2. rewrite Heqot1, Heqot2. repeat rewrite unfold_interp_mrec. cbn. inv H. + apply inj_pair2 in H1, H4. subst. gstep. constructor. gfinal. left. eapply CIH. eapply rutt_bind; eauto. intros. cbn in H. clear - H H0. specialize (H0 r1 r2 (sum_postrel_inl _ _ _ _ _ _ _ _ H)). pclearbot. auto. + apply inj_pair2 in H1, H4. subst. gstep. constructor. auto. intros. repeat rewrite tau_euttge. gfinal. left. eapply CIH. clear - H0 H. specialize (H0 a b (sum_postrel_inr _ _ _ _ _ _ _ _ H)). pclearbot. auto. - apply simpobs in Heqot1. rewrite Heqot1. rewrite unfold_interp_mrec at 1. cbn. rewrite tau_euttge. auto. - apply simpobs in Heqot2. rewrite Heqot2. setoid_rewrite unfold_interp_mrec at 2. cbn. rewrite tau_euttge. auto. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(ITree ITreeFacts Core.Subevent Basics.HeterogeneousRelations Eq.Rutt Props.Leaf)