proposition: Lemma Leaf_interp_inv {E F R} (h: E ~> itree F) (t: itree E R) x: x ∈ interp h t -> x ∈ t.
proof: Proof. intros Hleaf. apply (has_post_Leaf (interp h t) (fun x => x ∈ t)); auto. apply Leaf_interp_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)