fact: Definition gen_bind_aux {A B: Type} (f: A → M B): ∀ {s}, Term sign A s → Term sign B s := fix F {s} (t: Term sign A s): Term sign B s := match t with | Var _ _ v tt => f v | App _ _ o z x y => App _ _ _ z (F x) (F y) | Op _ _ o => Op _ _ o end.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.monads