fact: Definition primRecSigmaFormulaHelp (n : nat) (SigA SigB : Formula) : Formula := andH (existH 0 (andH SigA (substF2 βR 1 Zero 2 (var n.+2)))) (forallH n.+3 (impH (LT (var n.+3) (var n.+1)) (existH 0 (existH (S n) (andH (substF3 βR 1 (var n.+3) 2 (var n.+2) 0 (var n.+1)) (andH (substF SigB n.+2 (var n.+3)) (substF2 βR 1 (Succ (var (n.+3))) 2 (var n.+2)))))))).
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)