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