Author: Pierre Corbineau
Title: First-order reasoning in the calculus of inductive constructions
Abstract: 
We present a contraction-free sequent calculus including inductive
definitions for the first-order intuitionistic logic. We show that it
is a natural extension to Dyckhoff's LJT calculus and we prove the
contraction- and cut-elimination properties, thus extending
Dyckhoff's result, in order to validate its use as a basis for
proof-search procedures. Finally we describe the proof-search
strategy used in our implementation as a tactic in the Coq proof assistant.