fact: Definition checkPrfIMP2 (p recs : nat) := let A := car (cdr (cdr p)) in let B := car (cdr (cdr (cdr p))) in let C := cdr (cdr (cdr (cdr p))) in charFunction 2 Nat.eqb (cPair 1 (cPair (cPair 1 (cPair A (cPair 1 (cPair B C)))) (cPair 1 (cPair (cPair 1 (cPair A B)) (cPair 1 (cPair A C)))))) (car p).
imports: Coq(Arith Lia) hydras.Ackermann(primRec codeFreeVar codeSubFormula cPair code folProp extEqualNat wellFormed folProof prLogic) hydras(Compat815)