fact: Definition codeSubTermTerms : nat -> nat -> nat -> nat := evalStrongRec 2 (fun t recs v s : nat => cPair (switchPR (car t) (cPair (car t) (cdr (codeNth (t - S (cdr t)) recs))) (switchPR (charFunction 2 Nat.eqb (cdr t) v) s t)) (switchPR t (S (cPair (car (codeNth (t - S (car (pred t))) recs)) (cdr (codeNth (t - S (cdr (pred t))) recs)))) 0)).
imports: hydras.Ackermann(primRec cPair folProp code extEqualNat) Coq(Arith) hydras(Compat815) NewNotations