Why isn't a propositional computation rule for quotients enough to derive funext?

What question should the reference manual answer?

Why isn't a propositional computation rule for quotients enough to derive funext? This would satisfy curiosity about quotients and why they are the way they are in Lean.

Additional context
This was a request from a colleague reviewing the chapter on quotients pre-publication. Here's where the proof breaks:

axiom Q.{u} {α : Sort u} (r : α → α → Prop) : Sort u

axiom Q.mk.{u} {α : Sort u} (r : α → α → Prop) (a : α) : Q r

axiom Q.lift.{u, v} {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (a : ∀ (a b : α), r a b → Eq (f a) (f b)) :
  Q r → β

axiom Q.sound.{u} : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Q.mk r a = Q.mk r b


axiom Q.comp.{u,v} {α : Sort u} {r : α → α → Prop} {β : Sort v} {f : α → β} {prf : ∀ (a b : α), r a b → Eq (f a) (f b)} {a : α} : Q.lift f prf (Q.mk r a) = f a

theorem funext'' {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
    (h : ∀ x, f x = g x) : f = g := by
  let eqv (f g : (x : α) → β x) := ∀ x, f x = g x
  let extfunApp (f : Q eqv) (x : α) : β x :=
    Q.lift
      (fun (f : ∀ (x : α), β x) => f x)
      (fun _ _ h => h x)
      f

  suffices extfunApp (Q.mk eqv f) = extfunApp (Q.mk eqv g) by
    simp [extfunApp] at this
    /-
    α : Sort u
    β : α → Sort v
    f g : (x : α) → β x
    h : ∀ (x : α), f x = g x
    eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
    extfunApp : Q eqv → (x : α) → β x := fun f x => Q.lift (fun f => f x) ⋯ f
    this : (fun x => Q.lift (fun f => f x) ⋯ (Q.mk eqv f)) = fun x => Q.lift (fun f => f x) ⋯ (Q.mk eqv g)
    ⊢ f = g
    -/
    sorry
  exact congrArg extfunApp (Q.sound h)

The problem is that rewriting propositionally under a lambda requires funext, which we don't want to assume in the course of proving it. The definitional computation rule solves the problem by making the two sides defeq to fun x => f x and fun x => g x, which by eta is convertible with the desired goal.

Start with the reference manual's chapter on quotients and the Lean proof shown in the issue. Explain why the propositional computation rule leaves rewriting under the function lambda unresolved, while the definitional rule makes both sides definitionally equal to the expected functions. Done means the manual answers the question clearly and preserves the distinction without assuming funext.