fact: Definition checkPrfEQ5 (p recs : nat) := let f := cdr (cdr p) in notZero (codeArityF f) * charFunction 2 Nat.eqb (codeAxmEqHelp (pred (codeArityF f)) (cPair 0 (cPair (cPair (S f) (codeNVars1 (pred (codeArityF f)))) (cPair (S f) (codeNVars2 (pred (codeArityF f))))))) (car p).
imports: Coq(Arith Lia) hydras.Ackermann(primRec codeFreeVar codeSubFormula cPair code folProp extEqualNat wellFormed folProof prLogic) hydras(Compat815)