[raincole]

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.