proposition: Lemma has_post_Leaf {E R} (t: itree E R) Q r: has_post t Q -> r ∈ t -> Q r.
proof: Proof. intros Hcond Himage. rewrite has_post_post_strong in Hcond. destruct (Leaf_eutt_l t t r Hcond Himage). intuition; now subst. 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)