fact: Definition primRecSigmaFormula (n : nat) (SigA SigB : Formula) : Formula := existH n.+2 (andH (minimize (primRecSigmaFormulaHelp n SigA SigB) (primRecPiFormulaHelp n SigA SigB) n.+2 n.+4) (substF2 βR 2 (var n.+2) 1 (var n.+1))).
imports: Coq(Arith) hydras.Ackermann(extEqualNat subAll folProp subProp folReplace folLogic3 NN NNtheory primRec expressible) Coqprime(ChineseRem) Coq(Vector List Lia) hydras(ListExt cPair MoreDecidable) hydras(Compat815 ssrnat_extracts) Coq(Utf8)