Research proof index

On the table of all previously computed values, the step function returns the next one , the obligation Primrec.nat_strong_rec asks for. Four branches, matching ofNat's; the two atomic ones are arithmetic. In the func branch, natToVec succeeding is tested as natToList having the recorded length (natToVec_isSome_of_length/`natToVec_eq_none_of_l...

With every lookup present and non-zero, the fold rebuilds the vecToNat code of the arguments.

A stronger variant of (unique existence of) replacement, which only requires uniqueness on X. The statement of this lemma is thanks to tosiaki.

Restricting an inserted relation to a set that does not contain the inserted first coordinate recovers the original restriction.

getM at Option succeeds exactly when every component does. This is what turns the func branch of ofNat into a statement about each argument separately.

Recursive enumerability of a predicate on a Primcodable type is equivalent to the recursive enumerability of the corresponding predicate on ℕ obtained by decoding.