proposition: Lemma betaThm2 n (y : nat -> nat) : {a : nat * nat | forall z, z < n -> y z = β (cPair (fst a) (snd a)) z}.
proof: Proof. destruct (betaTheorem1 n y) as [x e]; exists (snd x, fst x). intros; unfold beta; rewrite !cPairProjections2, !cPairProjections1; simpl; now apply e. 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)