fact: Definition ReplaceTermTermsTerm : nat -> nat -> nat := evalStrongRec 1 (fun t recs s : nat => cPair (switchPR (car t) (cPair (car t) (cdr (codeNth (t - S (cdr t)) recs))) (cPair 0 s)) (switchPR t (S (cPair (car (codeNth (t - S (car (pred t))) recs)) (cdr (codeNth (t - S (cdr (pred t))) recs)))) 0)).
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)