fact: Definition checkPrfEQ2 (p recs : nat) := charFunction 2 Nat.eqb (cdr (cdr p)) 0 * charFunction 2 Nat.eqb (codeFormula (v#0 = v#1 -> v#1 = v#0)%fol) (car p).
imports: Coq(Arith Lia) hydras.Ackermann(primRec codeFreeVar codeSubFormula cPair code folProp extEqualNat wellFormed folProof prLogic) hydras(Compat815)