fact: Definition FixFun3Mod B {IB:Inhab B} (E:binary B) A1 A2 A3 (F:(A1->A2->A3->B)->(A1->A2->A3->B)) := curry3 (FixFunMod E (fun f' => uncurry3 (F (curry3 f')))).
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)