fact: Definition pmodify {I} (S : I → Type) {i} (f : S :→ S) : PState S (fun _ => unit) i := mkPState (fun s : S i => (tt, f i s)).
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple