sketch precise narrowing + exp_preserves_sub as one big mutual induction, seems to work so far EXCEPT what is the termination measure??