proposition: Lemma mrec_rutt (A B : Type) (d1 : D1 A) (d2 : D2 B) : RPreInv A B d1 d2 -> rutt RPre RPost (fun (a : A) (b : B) => RPostInv A B d1 a d2 b) (mrec bodies1 d1) (mrec bodies2 d2).
proof: Proof. intros. apply interp_mrec_rutt. auto. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(ITree ITreeFacts Core.Subevent Basics.HeterogeneousRelations Eq.Rutt Props.Leaf)