  This paper presents a cut-elimination proof for the logic $LG^\omega$, which
is an extension of a proof system for encoding generic judgments, the logic
$\FOLDNb$ of Miller and Tiu, with an induction principle. The logic
$LG^\omega$, just as $\FOLDNb$, features extensions of first-order
intuitionistic logic with fixed points and a ``generic quantifier'', $\nabla$,
which is used to reason about the dynamics of bindings in object systems
encoded in the logic. A previous attempt to extend $\FOLDNb$ with an induction
principle has been unsuccessful in modeling some behaviours of bindings in
inductive specifications. It turns out that this problem can be solved by
relaxing some restrictions on $\nabla$, in particular by adding the axiom $B
\equiv \nabla x. B$, where $x$ is not free in $B$. We show that by adopting the
equivariance principle, the presentation of the extended logic can be much
simplified. This paper contains the technical proofs for the results stated in
\cite{tiu07entcs}; readers are encouraged to consult \cite{tiu07entcs} for
motivations and examples for $LG^\omega.$
