Does anyone direct me to a paper detailing a cut-elimination theorem for propositional intuitionistic logic, including an inductive datatype such as the natural numbers (lists or trees would be fine, too)? An example of the kind of system I am interested in is Godel's T, which has types given by the grammar $A ::= \mathbb{N} \;\;|\;\; A \to A'$. I am not very interested in quantifiers over natural numbers or predicates indexed by natural numbers. I know how to prove beta-normalization for natural deduction version of these systems using a logical relations argument (or related techniques such as NbE), but would like to know if there are standard references on how to adapt these methods to sequent calculi. The reason I ask is that I am studying adding fixed point operators for guarded recursion to a language. The denotational idea is a rather old one -- interpret types as ultrametric spaces and fixed points via Banach's theorem -- but the purely syntactic techniques I know for proving cut-elimination don't seem to adapt that well. 
Cut-elimination for calculus with nats or other inductive datatype?
lo.logic;pl.programming languages;sequent calculus
How about Ulrich Berger's work? For example Strong normalization for applied lambda calculi. The recursively defined constants part gets you inductive types, more or less. And don't be put off by the word untyped, he gets results for typed systems too.