generated at
Calculus of Inductive Constructions
https://coq.inria.fr/refman/language/cic.html
Coqの型システム
https://en.wikipedia.org/wiki/Calculus_of_constructions