Introduction to the Calculus of Inductive Constructions