fact: Definition wellFormedTermTerms : nat -> nat := evalStrongRec 0 (fun t recs : nat => cPair (switchPR (cPairPi1 t) (charFunction 2 Nat.eqb (codeArityF (pred (cPairPi1 t))) (S (codeLength (cPairPi2 t))) * cPairPi2 (codeNth (t - S (cPairPi2 t)) recs)) 1) (switchPR t (cPairPi1 (codeNth (t - S (cPairPi1 (pred t))) recs) * cPairPi2 (codeNth (t - S (cPairPi2 (pred t))) recs)) 1)).
imports: hydras.Ackermann(primRec cPair) Coq(Arith Lia) hydras.Ackermann(code folProp extEqualNat codeList) hydras(Compat815)