proposition: Lemma betaThm5 : forall (n : nat) (y : nat -> nat), {a : nat * nat | forall z : nat, z < n -> y z = Usual.β (fst a) (snd a) z }.
proof: Proof. intros n y; destruct (betaTheorem1 n y) as [x e]. unfold Usual.β; now exists x. 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)