Function derive_quot_rec 

pub fn derive_quot_rec(ctx: &Context) -> KernelResult<(Term, Term)>

Quot_rec — the DEPENDENT quotient eliminator, built from the four quotient primitives rather than taken as a fifth one. The prelude registers exactly this body as Quot_rec.

Lean does not assume it either. init_quot (Init/Core.lean:1515–1527) introduces exactly Quot, Quot.mk, Quot.lift and Quot.ind, alongside the Quot.sound axiom — four constants and one axiom, not five. Quot.rec is a protected abbrev assembled from them at Init/Core.lean:1581–1611, and #print axioms Quot.rec answers [Quot.sound]: it costs the trusted base nothing beyond the axiom already paid for. The recipe below is Lean’s, transcribed constant for constant:

indep f a             := ⟨Quot_mk a, f a⟩              : PSigma (Quot A r) motive
indepCoherent f h a b := PSigma.eta (Quot_sound p) (h a b p)
L                     := Quot_lift A r (PSigma Q motive) indep indepCoherent
liftIndepPr1 q        : PSigma_fst (L q) = q           -- Quot_ind, then refl
Quot_rec … q          := liftIndepPr1 q ▸ PSigma_snd (L q)

The two computation steps that make it work are already in the kernel: Quot_lift … (Quot_mk a) ⤳ indep a is the one ι-rule quotients have, and PSigma_fst (PSigma_mk x y) ⤳ x is an ordinary structure projection. So PSigma_fst (L (Quot_mk a)) reduces to Quot_mk a and the liftIndepPr1 obligation is discharged by refl in every branch Quot_ind produces — which is exactly why Lean’s proof is induction q using Quot.ind; exact rfl.

PSigma.eta is inlined rather than registered: it is used once, and Lean’s own (Init/Core.lean:1272–1276) is two substs, which is two Eq_rec_dep transports here.

The pair is PSigma, not Sigma, for the reason Lean’s is: the carrier is Sort u, so the pair lives in Sort (max 1 u) and Quot_lift reaches it through its own target level. Every reference is a bare global whose levels the application rule solves at each use, so the only level the body names is its carrier binder’s, which β removes wherever the eliminator is applied. The motive is Quot A r → Type 0, the prelude statement’s own; Lean’s is Sort v.