fact: Definition codeLength : nat -> nat := evalStrongRec 0 (fun n Hrecs : nat => switchPR n (S (codeNth (n - S (cPairPi2 (pred n))) Hrecs)) 0).
imports: hydras.Ackermann(primRec cPair) hydras.Ackermann(ListExt) Coq(Arith) hydras(extEqualNat Compat815)