Why Coq does not allow the containment relationship between types

Thank you for reposting this question in your preferred language! I’ve added my thoughts there:

I’m so happy that this multilingual forum is helping people to learn Coq more efficiently.