proposition: Lemma has_post_iter_strong : forall {E R I} (body : I -> itree E (I + R)) (entry : I) (Inv : I -> Prop) (Q : R -> Prop), (forall i, Inv i -> body i ⤳ sum_pred Inv Q) -> Inv entry -> ITree.iter body entry ⤳ Q.
proof: Proof. intros * IND INIT. eapply (@KTreeFacts.eutt_iter_gen _ _ _ (fun x y => x = y /\ Inv x)); eauto. intros i ? [<- ?]. specialize (IND i); apply has_post_post_strong in IND; auto. unfold has_post_strong in IND. eapply eqit_mon; try apply IND; auto. intros [] ? [<- ?]; eauto. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Basics.Utils ITree Eq.Eqit Basics.HeterogeneousRelations Interp.TranslateFacts)