fact: Definition composeSigmaFormula (n w m : nat) (A : Vector.t (Formula * naryFunc n) m) (B : Formula) : Formula := addExists (S w) m (andH (FormulasToFormula n w m A) (subAllFormula LNN B (fun x : nat => match x with | O => var 0 | S x' => var (S x' + w) end))).
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)