proposition: Lemma Leaf_iter_inv {E R I}: forall (body: I -> itree E (I + R)) (entry: I) (Inv: I -> Prop) (Q: R -> Prop), (forall i r, Inv i -> r ∈ body i -> sum_pred Inv Q r) -> Inv entry -> forall r, r ∈ (ITree.iter body entry) -> Q r.
proof: Proof. intros * Hinv Hentry. rewrite <- has_post_Leaf_equiv. eapply has_post_iter_strong; eauto. setoid_rewrite has_post_Leaf_equiv. eauto. 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)