fact: Fixpoint codeTerm (t : Term) : nat := match t with | var n => cPair 0 n | apply f ts => cPair (S (codeF cl f)) (codeTerms _ ts) end with codeTerms (n : nat) (ts : Terms n) {struct ts} : nat := match ts with | Tnil => 0 | Tcons n t ss => S (cPair (codeTerm t) (codeTerms n ss)) end.
imports: Coq(Arith) hydras.Ackermann(fol folProof cPair)