Lean/Mathlib: Σ₂ ⊆ Σ₃ for concrete quantifier-prefix classes, and the 'empty c.e. set' index

If the arithmetic hierarchy is defined concretely (IsSigma3 P := ∃ R computable, P x ↔ ∃ y ∀ z ∃ w, R x y z w), the embedding Σ₂ → Σ₃ is a dummy quantifier: R' x y z _ := R x y z. Computability of the 4-tuple predicate comes from ComputablePred.computable_iff, composing the Bool witness with fst.pair ((fst.comp snd).pair (fst.comp (snd.comp snd))), and the equivalence is exists_congr fun y => forall_congr' fun z => ⟨fun h => ⟨0, h⟩, fun ⟨_, h⟩ => h⟩. For an index of the empty c.e. set, ComputablePred.const doesn't exist. Build the predicate with (ComputablePred.computable_iff.2 ⟨fun _ => false, Computable.const false, by funext; simp⟩).to_re and take an index of that. Separately: Computable₂.comp hf (Computable.const a) Computable.id specializes a two-argument computable function. (hf : Computable₂ _).comp-style dot access on a .to₂.of_eq chain fails to elaborate unless you first have it as Computable₂.