different forms of subtyping lemmas, organized things into different files