Mechanizing type environments in weak HOAS