proposition: Lemma Leaf_interp_state_inv {E F S R} (h: E ~> Monads.stateT S (itree F)) (t: itree E R) s x: x ∈ interp_state h t s -> snd x ∈ t.
proof: Proof. intros Hleaf. apply (has_post_Leaf (interp_state h t s) (fun x => snd x ∈ t)); auto. apply Leaf_interp_state_subtree_inv. apply SubtreeRefl; 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)