fact: Definition codeFreeVarListFormula : nat -> nat := evalStrongRec 0 (fun l recs : nat => switchPR l (codeApp (codeFreeVarFormula (car (pred l))) (codeNth (l - S (cdr (pred l))) recs)) 0).
imports: hydras.Ackermann(primRec cPair) Coq(List Arith) hydras.Ackermann(ListExt) hydras(folProp code Compat815)