I have a little experience of both Coq and Lean and have followed some of the discussion about Lean's handling of quotient types. I have seen computer scientis

I have a little experience of both Coq and Lean and have followed some of the discussion about Lean's handling of quotient types. I have seen computer scientists emphasise to mathematicians that subject reduction should not be forfeit but I have yet to see a convincing argument/example for why not. I don't suppose you can elaborate on why this may be / is so crazy, that someone with only a limited understanding of type theory might follow?