fact: Definition evalStrongRecHelp (n : nat) (f : naryFunc n.+2) : naryFunc n.+1 := evalPrimRecFunc n (evalComposeFunc n 0 (Vector.nil _) (codeList nil)) (evalComposeFunc n.+2 2 (Vector.cons _ f _ (Vector.cons _ (evalProjFunc n.+2 n (Nat.lt_lt_succ_r _ _ (Nat.lt_succ_diag_r _))) _ (Vector.nil _))) (fun a b : nat => S (cPair a b))).
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec) Extraction