Coqのすごいのは、inductionといって何かしらの概念の定義（どういったものを用意するとそれが作れるか）から、自動的にそれにまつわる公理が定義されるところ
これは自然数の帰納法を一般化したもの …