The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,
I don't know what you mean by "write the term". Do you mean "prove"?
If yes then you can look at the definition of, say, nat_ind by doing:
"Print nat_ind."
You get something like this.

fix F (n : nat) : P n :=
  match n as n0 return (P n0) with
  | 0 => f
  | S n0 => f0 n0 (F n0)
  end.

Notice the form "fix F n .. := match n with ....end"
This Fix + match is the core structure of the proofs of induction
principles: it is the nominal application of the elimination mechanism
at the heart of CIC.

Hope this helps.
P.