proposition: Lemma to_hoare_post_bind_assoc `{MayProvide ix i} `(c : contract i Ω) `(p : impure ix a) `(f : a -> impure ix b) `(Hp : post (to_hoare c (impure_bind p f)) ω x ω') : exists y ω'', post (to_hoare c p) ω y ω'' /\ post (to_hoare c $ f y) ω'' x ω'.
proof: Proof. revert ω Hp. induction p; intros ω Hp. + now exists x0, ω. + destruct Hp as [y [ω'' [Hp1 Hp2]]]. apply H0 in Hp2. destruct Hp2 as [z [ω''' [Hp2 Hp3]]]. exists z, ω'''. split; [| apply Hp3]. exists y, ω''. now split. Qed.
imports: FreeSpec.Core(Interface ImpureFacts Contract)