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