proposition: Lemma Leaf_interp_state_subtree_inv {E F S R} (h: E ~> Monads.stateT S (itree F)) (t u: itree E R) (s: S): subtree u t -> has_post (interp_state h u s) (fun x => snd x ∈ t).
proof: Proof. revert t u s. ginit. gcofix CIH; intros * Hsub. rewrite (itree_eta u) in Hsub. rewrite ! unfold_interp_state. 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 [u1 u2] _ <-; cbn. 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)