I am not familiar with the formal type theory, but this one is intuitive if you view it this way: 1. When A is a subtype of B, it means A can be used as B (a T

I am not familiar with the formal type theory, but this one is intuitive if you view it this way: 1. When A is a subtype of B, it means A can be used as B (a Teacher can be used by any function that accepts a Human). 2. static lifetime lives longer any other lifetimes, so it can be used as other lifetimes.