List 破坏了 Monad
如果 M 是 1 到 n 个结果的计算，bind 需要 lift_asrt，bind 不满足结合律。
bind (bind m f) g 类似于 BFS， bind m (fun x => bind (f x) g) 类似于 DFS。
coq
Definition M A :=
assertion -> option (list (A * assrtion)).
Definition bind {A B} (m : M A) (f : A -> M B) : M B :=
fun asrt =>
do res <- m asrt ;
lift_asrt f res.