proposition: Lemma has_post_Leaf_equiv {E R} (t: itree E R) Q: has_post t Q <-> (forall r, r ∈ t -> Q r).
proof: Proof. intuition. eapply has_post_Leaf; eauto. revert t H. pcofix CIH; intros t Hpost. pstep; red. setoid_rewrite (itree_eta t) in Hpost. desobs t Ht; clear t Ht. - constructor. apply Hpost, Leaf_Ret. - constructor. right; apply CIH. intros. apply Hpost, Leaf_Tau, H. - constructor. intros. right. apply CIH. intros. eapply Hpost, Leaf_Vis, H. 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)