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)
<?xml version="1.0" encoding="ISO-8859-1"?>
<!DOCTYPE Definition SYSTEM "http://localhost:8081/getdtd?url=cic.dtd">
<Definition name="nat_ind" params="">
<body>
<LAMBDA>
<source>
<PROD>
<source>
<MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
</source>
<target>
<SORT value="Prop"/>
</target>
</PROD>
</source>
<target binder="P">
<LAMBDA>
<source>
<APPLY>
<REL value="1" binder="P"/>
<MUTCONSTRUCT uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0" noConstr="1"/>
</APPLY>
</source>
<target binder="f">
<LAMBDA>
<source>
<PROD>
<source>
<MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
</source>
<target binder="n">
<PROD>
<source>
<APPLY>
<REL value="3" binder="P"/>
<REL value="1" binder="n"/>
</APPLY>
</source>
<target>
<APPLY>
<REL value="4" binder="P"/>
<APPLY>
<MUTCONSTRUCT uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0" noConstr="2"/>
<REL value="2" binder="n"/>
</APPLY>
</APPLY>
</target>
</PROD>
</target>
</PROD>
</source>
<target binder="f0">
<FIX noFun="0">
<FixFunction name="F" recIndex="0">
<type>
<PROD>
<source>
<MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
</source>
<target binder="n">
<APPLY>
<REL value="4" binder="P"/>
<REL value="1" binder="n"/>
</APPLY>
</target>
</PROD>
</type>
<body>
<LAMBDA>
<source>
<MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
</source>
<target binder="n">
<MUTCASE uriType="cic:/coq/INIT/Datatypes/nat.ind" noType="0">
<patternsType>
<REL value="5" binder="P"/>
</patternsType>
<inductiveTerm>
<REL value="1" binder="n"/>
</inductiveTerm>
<pattern>
<REL value="4" binder="f"/>
</pattern>
<pattern>
<LAMBDA>
<source>
<MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
</source>
<target binder="n0">
<APPLY>
<REL value="4" binder="f0"/>
<REL value="1" binder="n0"/>
<APPLY>
<REL value="3" binder="F"/>
<REL value="1" binder="n0"/>
</APPLY>
</APPLY>
</target>
</LAMBDA>
</pattern>
</MUTCASE>
</target>
</LAMBDA>
</body>
</FixFunction>
</FIX>
</target>
</LAMBDA>
</target>
</LAMBDA>
</target>
</LAMBDA>
</body>
<type>
<CAST>
<term>
<PROD>
<source>
<PROD>
<source>
<MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
</source>
<target>
<SORT value="Prop"/>
</target>
</PROD>
</source>
<target binder="P">
<PROD>
<source>
<APPLY>
<REL value="1" binder="P"/>
<MUTCONSTRUCT uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0" noConstr="1"/>
</APPLY>
</source>
<target binder="f">
<PROD>
<source>
<PROD>
<source>
<MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
</source>
<target binder="n">
<PROD>
<source>
<APPLY>
<REL value="3" binder="P"/>
<REL value="1" binder="n"/>
</APPLY>
</source>
<target>
<APPLY>
<REL value="4" binder="P"/>
<APPLY>
<MUTCONSTRUCT uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0" noConstr="2"/>
<REL value="2" binder="n"/>
</APPLY>
</APPLY>
</target>
</PROD>
</target>
</PROD>
</source>
<target binder="f0">
<PROD>
<source>
<MUTIND uri="cic:/coq/INIT/Datatypes/nat.ind" noType="0"/>
</source>
<target binder="n">
<APPLY>
<REL value="4" binder="P"/>
<REL value="1" binder="n"/>
</APPLY>
</target>
</PROD>
</target>
</PROD>
</target>
</PROD>
</target>
</PROD>
</term>
<type>
<SORT value="Prop"/>
</type>
</CAST>
</type>
</Definition>