fact: Definition ibind `{m : PMonad} {i j k a b} : Atkey m i j a → (a → Atkey m j k b) → Atkey m i k b := fun x f => angbind f _ x.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple