theorem Std.Do.except_ok_spec {α ε : Type} {x : α} {pre : Prop} {post : α → Prop} {error : ε → Prop} (h : ∀ (r : α), r = x ∧ pre → post r) : ⦃⌜pre⌝⦄ Except.ok x ⦃(fun (a : α) => ⌜post a⌝, fun (e : ε) => ⌜error e⌝, ())⦄

theorem Std.Do.Except.by_wp {ε α : Type} {x : α} {prog : Except ε α} (h : prog = Except.ok x) {P : α → Prop} {Q : ε → Prop} : (⊢ₛ wp⟦prog⟧ (fun (r : α) => ⌜P r⌝, fun (e : ε) => ⌜Q e⌝, ())) → P x

theorem Std.Do.StateT.by_wp {α σ : Type} {x : α × σ} {s : σ} {prog : StateT σ Id α} (h : prog.run s = x) {P : α → σ → Prop} : (⊢ₛ wp⟦prog⟧ (fun (r : α) (s : σ) => ⌜P r s⌝, ()) s) → P x.fst x.snd

theorem Std.Do.StateT.Except.by_wp {α σ ε : Type} {x : α × σ} {s : σ} {prog : StateT σ (Except ε) α} (h : prog s = Except.ok x) {P : α → Prop} {Q : ε → Prop} : (⊢ₛ wp⟦prog⟧ (fun (r : α) (x : σ) => ⌜P r⌝, fun (e : ε) => ⌜Q e⌝, ()) s) → P x.fst