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