proposition: Theorem primRecRepresentable : forall (n : nat) (f : naryFunc n) (p : isPR n f), Representable n f (primRecFormula n (fun2PR f)).
proof: Proof. intros n f p. assert (H: Representable n (evalPrimRec n (proj1_sig p)) (primRecFormula n (proj1_sig p))) by apply primRecRepresentable1. destruct H as [H H0]; split. - assumption. - destruct p as (x, p); eapply Representable_ext with (evalPrimRec n x); assumption. Qed.
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)