fact: Definition mfix3 A B C D (ff:(A -> B -> C -> m D) -> (A -> B -> C -> m D)) (a:A) (b:B) (c:C) : m D := let ff' fabcp (abcp:A*B*C) := let (abp,c) := abcp in let (a,b) := abp in let fabc a b c := fabcp (a,b,c) in ff fabc a b c in mfix ff' (a,b,c).
imports: ExtLib.Structures.Monad