fact: Definition checkPrfEQ1 (p recs : nat) := charFunction 2 Nat.eqb (cdr (cdr p)) 0 * charFunction 2 Nat.eqb (codeFormula (equal (var 0) (var 0))) (car p).
imports: Coq(Arith Lia) hydras.Ackermann(primRec codeFreeVar codeSubFormula cPair code folProp extEqualNat wellFormed folProof prLogic) hydras(Compat815)