Eta-expand newtype coercions in External Core