fact: Definition LIP_mfold_left {A} f := fix loop (l : LIP) (a : A) {struct l} : M A := match l with | lnil => M.ret a | lcons b bs => f a b >>= loop bs end%MC.
imports: Coq.Strings.String Mtac2(List Base) Mtac2.tactics(TacticsBase Tactics ImportedTactics)