English
If R is decidable, then the universal mem-list relation (L,b) ↦ ∀ a ∈ L, R(a,b) is primitive recursive.
Русский
Если R разрешимо, то универсальное отношение в перечне L для b примитивно-рекурсивно.
LaTeX
$$$\mathrm{PR}\big( (L,b) \mapsto \forall a \in L\, R(a,b) \big).$$$
Lean4
theorem subtype_val_iff {p : β → Prop} [DecidablePred p] {hp : PrimrecPred p} {f : α → Subtype p} :
haveI := Primcodable.subtype hp
(Primrec fun a => (f a).1) ↔ Primrec f :=
by
letI := Primcodable.subtype hp
refine ⟨fun h => ?_, fun hf => subtype_val.comp hf⟩
refine Nat.Primrec.of_eq h fun n => ?_
rcases @decode α _ n with - | a; · rfl
simp; rfl