proposition: Lemma Leaf_interp_subtree_inv {E F R} (h: E ~> itree F) (t u: itree E R): subtree u t -> has_post (interp h u) (fun x : R => x ∈ t).
proof: Proof. revert t u. ginit. gcofix CIH; intros * Hsub. rewrite (itree_eta u) in Hsub. rewrite ! unfold_interp. desobs u Hu; clear u Hu; cbn. - gstep; red. constructor. eapply subtree_image; eauto. apply Leaf_Ret. - gstep; red. constructor. gfinal; left. apply CIH. apply SubtreeTau, Hsub. - guclo eqit_clo_bind; econstructor. reflexivity. intros u _ <-. gstep; red. constructor. gfinal; left. apply CIH. eapply SubtreeVis, Hsub. 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)