Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions - Bertot, Yves.; Casteran, P. (Pierre) (Springer, 2004)