fact: Fixpoint codeFormula (f : Formula) : nat := match f with | equal t1 t2 => cPair 0 (cPair (codeTerm t1) (codeTerm t2)) | impH f1 f2 => cPair 1 (cPair (codeFormula f1) (codeFormula f2)) | notH f1 => cPair 2 (codeFormula f1) | forallH n f1 => cPair 3 (cPair n (codeFormula f1)) | atomic R ts => cPair (4 + codeR cl R) (codeTerms _ ts) end.
imports: Coq(Arith) hydras.Ackermann(fol folProof cPair)