Encoding CIC in XML: an example of exported object

The principle of induction over natural numbers in Coq:

  Coq < Print nat_ind.
  nat_ind = 
  [P:(nat->Prop); f:(P O); f0:((n:nat)(P n)->(P (S n)))]
   Fix F
     {F [n:nat] : (P n) :=
        Cases n of
          O => f
        | (S n0) => (f0 n0 (F n0))
        end}
       : (P:(nat->Prop))(P O)->((n:nat)(P n)->(P (S n)))->(n:nat)(P n)