Coercion from Subtype to Exists

Stream: lean4

[Tom Kranz]

I'm curious about why https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Subtype.existsOfSubtype is not incorporated in a coercion. Naïvely, I'd think that it'd be neat if Subtype members were automatically treated as Exists proofs, but I'm wondering if there's a deeper reason for the lack of such a Coe instance.