Verification of Substitution Theorem Using HOL. - Takayuki Koai; Makoto Tatsuta (Inf. Media Technol., 2012)