We should be able to reason about types of HOL to efficiently produce types.
We should be able to reason about types of HOL to efficiently produce types.