proposition: Lemma fix_ack : forall m n, ack m n = Ack ack m n.
proof: Proof. Proof using. applys~ (FixFun2_fix (lexico2 (@lt nat _) (@lt nat _))). introv IH. unfolds. case_if~. case_if~. apply IH. emaths. rewrite IH. fequals~. emaths. emaths. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat