# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1563577460 -32400
# Node ID f5b3f30fcb162a3f332dcf9c4e9e0a292c154d87
# Parent  a1b5b890b7968240d45c32602b6e937824234e19# Parent  ecb329ba38ac904913313f2dd03ae2329039ffa6
ε-induction