fact: Definition fappgl {A B C} (comb : C -> C -> M C) (f : M ((A -> B) *m C)) (x : M (A *m C)) : M (B *m C) := (f >>= (fun '(m: b, cb) => '(m: a, ca) <- x; c <- comb cb ca; M.ret (m: b a, c) ) )%MC.
imports: Mtac2(Base Datatypes List Sorts tactics.Tactics) Strings.String