proposition: Lemma Leaf_interp_iter_inv {E F R I} (h: E ~> itree F): forall (body: I -> itree E (I + R)) (entry: I) (Inv: I -> Prop) (Q: R -> Prop), (forall i r, Inv i -> r ∈ interp h (body i) -> sum_pred Inv Q r) -> Inv entry -> forall r, r ∈ interp h (ITree.iter body entry) -> Q r.
proof: Proof. intros * Hbody Hentry r Hr. apply (Leaf_iter_inv (fun i => interp h (body i)) entry Inv); auto. rewrite (interp_iter' _ _ (fun i => interp h (body i))) in Hr. apply Hr. 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)