fact: Definition checkPrfAXM (p recs : nat) := switchPR (charFunction 2 Nat.eqb (cddr p) (car p)) (S (S (cPair (car p) 0))) 0.
imports: Coq(Arith Lia) hydras.Ackermann(primRec codeFreeVar codeSubFormula cPair code folProp extEqualNat wellFormed folProof prLogic) hydras(Compat815)