tatsuta's proof macros