A Gentzen-style sequent calculus of constructions with expansion rules

AbstractA Gentzen-style L-formulation of the calculus of constructions is presented and proved equivalent to a natural deduction formulation based on that of Seldin (1997). The L-rules corresponding to the conversion rules of the natural deduction system are expansion rules. Cut elimination follows from the equivalence to the natural deduction formulation and the normalization theorem for the latter