fact: Definition Ack ack m n := If m = 0 then n+1 else If n = 0 then ack (m-1) 1 else ack (m-1) (ack m (n-1)).
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat