fact: Definition liftM3 {x y z w : Type@{d}} (f : x → y → z → w) : F x → F y → F z → F w := Eval cbv beta iota zeta delta [ liftM2 ] in λ x y z, bind x (λ x, liftM2 (f x) y z).
imports: Category.Lib Category.Theory.Coq.Applicative