fact: Definition codeAxmEqHelp (n f : nat) : nat := nat_rec (fun _ => nat) f (fun m rec : nat => cPair 1 (cPair (cPair 0 (cPair (cPair 0 (m + m)) (cPair 0 (S (m + m))))) rec)) n.
imports: Coq(Arith Lia) hydras.Ackermann(primRec codeFreeVar codeSubFormula cPair code folProp extEqualNat wellFormed folProof prLogic) hydras(Compat815)