Preserve sections about typing rules in CIC chapter.

1 files changed, 1 insertions, 1521 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index b125d21a3c..5f74958712 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1,7 +1,4 @@
-.. _calculusofinductiveconstructions:
-
-
-Calculus of Inductive Constructions
+Typing rules
 ====================================
 
 The underlying formal language of |Coq| is a *Calculus of Inductive
@@ -24,95 +21,6 @@ to a type and takes the form “*for all x of type* :math:`T`, :math:`P`”. The
 “:math:`x` *of type* :math:`T`” is written “:math:`x:T`”. Informally, “:math:`x:T`” can be thought as
 “:math:`x` *belongs to* :math:`T`”.
 
-The types of types are called :gdef:`sort`\s. Types and sorts are themselves terms
-so that terms, types and sorts are all components of a common
-syntactic language of terms which is described in Section :ref:`terms`.  But
-first, we describe sorts.
-
-
-.. _Sorts:
-
-Sorts
-~~~~~~~~~~~
-
-All sorts have a type and there is an infinite well-founded typing
-hierarchy of sorts whose base sorts are :math:`\SProp`, :math:`\Prop`
-and :math:`\Set`.
-
-The sort :math:`\Prop` intends to be the type of logical propositions. If :math:`M` is a
-logical proposition then it denotes the class of terms representing
-proofs of :math:`M`. An object :math:`m` belonging to :math:`M` witnesses the fact that :math:`M` is
-provable. An object of type :math:`\Prop` is called a proposition.
-
-The sort :math:`\SProp` is like :math:`\Prop` but the propositions in
-:math:`\SProp` are known to have irrelevant proofs (all proofs are
-equal). Objects of type :math:`\SProp` are called strict propositions.
-See :ref:`sprop` for information about using
-:math:`\SProp`, and :cite:`Gilbert:POPL2019` for meta theoretical
-considerations.
-
-The sort :math:`\Set` intends to be the type of small sets. This includes data
-types such as booleans and naturals, but also products, subsets, and
-function types over these data types.
-
-:math:`\SProp`, :math:`\Prop` and :math:`\Set` themselves can be manipulated as ordinary terms.
-Consequently they also have a type. Because assuming simply that :math:`\Set`
-has type :math:`\Set` leads to an inconsistent theory :cite:`Coq86`, the language of
-|Cic| has infinitely many sorts. There are, in addition to the base sorts,
-a hierarchy of universes :math:`\Type(i)` for any integer :math:`i ≥ 1`.
-
-Like :math:`\Set`, all of the sorts :math:`\Type(i)` contain small sets such as
-booleans, natural numbers, as well as products, subsets and function
-types over small sets. But, unlike :math:`\Set`, they also contain large sets,
-namely the sorts :math:`\Set` and :math:`\Type(j)` for :math:`j<i`, and all products, subsets
-and function types over these sorts.
-
-Formally, we call :math:`\Sort` the set of sorts which is defined by:
-
-.. math::
-
-   \Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\}
-
-Their properties, such as: :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and
-:math:`\Type(i):\Type(i+1)`, are defined in Section :ref:`subtyping-rules`.
-
-The user does not have to mention explicitly the index :math:`i` when
-referring to the universe :math:`\Type(i)`. One only writes :math:`\Type`. The system
-itself generates for each instance of :math:`\Type` a new index for the
-universe and checks that the constraints between these indexes can be
-solved. From the user point of view we consequently have :math:`\Type:\Type`. We
-shall make precise in the typing rules the constraints between the
-indices.
-
-
-.. _Implementation-issues:
-
-**Implementation issues** In practice, the Type hierarchy is
-implemented using *algebraic
-universes*. An algebraic universe :math:`u` is either a variable (a qualified
-identifier with a number) or a successor of an algebraic universe (an
-expression :math:`u+1`), or an upper bound of algebraic universes (an
-expression :math:`\max(u_1 ,...,u_n )`), or the base universe (the expression
-:math:`0`) which corresponds, in the arity of template polymorphic inductive
-types (see Section
-:ref:`well-formed-inductive-definitions`),
-to the predicative sort :math:`\Set`. A graph of
-constraints between the universe variables is maintained globally. To
-ensure the existence of a mapping of the universes to the positive
-integers, the graph of constraints must remain acyclic. Typing
-expressions that violate the acyclicity of the graph of constraints
-results in a Universe inconsistency error.
-
-.. seealso:: Section :ref:`printing-universes`.
-
-
-.. _Terms:
-
-Terms
-~~~~~
-
-
-
 Terms are built from sorts, variables, constants, abstractions,
 applications, local definitions, and products. From a syntactic point
 of view, types cannot be distinguished from terms, except that they
@@ -411,221 +319,6 @@ following rules.
    :math:`x` may be used in a conversion rule
    (see Section :ref:`Conversion-rules`).
 
-
-.. _Conversion-rules:
-
-Conversion rules
---------------------
-
-In |Cic|, there is an internal reduction mechanism. In particular, it
-can decide if two programs are *intentionally* equal (one says
-*convertible*). Convertibility is described in this section.
-
-
-.. _beta-reduction:
-
-β-reduction
-~~~~~~~~~~~
-
-We want to be able to identify some terms as we can identify the
-application of a function to a given argument with its result. For
-instance the identity function over a given type :math:`T` can be written
-:math:`λx:T.~x`. In any global environment :math:`E` and local context
-:math:`Γ`, we want to identify any object :math:`a` (of type
-:math:`T`) with the application :math:`((λ x:T.~x)~a)`.  We define for
-this a *reduction* (or a *conversion*) rule we call :math:`β`:
-
-.. math::
-
-        E[Γ] ⊢ ((λx:T.~t)~u)~\triangleright_β~\subst{t}{x}{u}
-
-We say that :math:`\subst{t}{x}{u}` is the *β-contraction* of
-:math:`((λx:T.~t)~u)` and, conversely, that :math:`((λ x:T.~t)~u)` is the
-*β-expansion* of :math:`\subst{t}{x}{u}`.
-
-According to β-reduction, terms of the *Calculus of Inductive
-Constructions* enjoy some fundamental properties such as confluence,
-strong normalization, subject reduction. These results are
-theoretically of great importance but we will not detail them here and
-refer the interested reader to :cite:`Coq85`.
-
-
-.. _iota-reduction:
-
-ι-reduction
-~~~~~~~~~~~
-
-A specific conversion rule is associated to the inductive objects in
-the global environment. We shall give later on (see Section
-:ref:`Well-formed-inductive-definitions`) the precise rules but it
-just says that a destructor applied to an object built from a
-constructor behaves as expected. This reduction is called ι-reduction
-and is more precisely studied in :cite:`Moh93,Wer94`.
-
-
-.. _delta-reduction:
-
-δ-reduction
-~~~~~~~~~~~
-
-We may have variables defined in local contexts or constants defined
-in the global environment. It is legal to identify such a reference
-with its value, that is to expand (or unfold) it into its value. This
-reduction is called δ-reduction and shows as follows.
-
-.. inference:: Delta-Local
-
-   \WFE{\Gamma}
-   (x:=t:T) ∈ Γ
-   --------------
-   E[Γ] ⊢ x~\triangleright_Δ~t
-
-.. inference:: Delta-Global
-
-   \WFE{\Gamma}
-   (c:=t:T) ∈ E
-   --------------
-   E[Γ] ⊢ c~\triangleright_δ~t
-
-
-.. _zeta-reduction:
-
-ζ-reduction
-~~~~~~~~~~~
-
-|Coq| allows also to remove local definitions occurring in terms by
-replacing the defined variable by its value. The declaration being
-destroyed, this reduction differs from δ-reduction. It is called
-ζ-reduction and shows as follows.
-
-.. inference:: Zeta
-
-   \WFE{\Gamma}
-   \WTEG{u}{U}
-   \WTE{\Gamma::(x:=u:U)}{t}{T}
-   --------------
-   E[Γ] ⊢ \letin{x}{u:U}{t}~\triangleright_ζ~\subst{t}{x}{u}
-
-
-.. _eta-expansion:
-
-η-expansion
-~~~~~~~~~~~
-
-Another important concept is η-expansion. It is legal to identify any
-term :math:`t` of functional type :math:`∀ x:T,~U` with its so-called η-expansion
-
-.. math::
-   λx:T.~(t~x)
-
-for :math:`x` an arbitrary variable name fresh in :math:`t`.
-
-
-.. note::
-
-   We deliberately do not define η-reduction:
-
-   .. math::
-      λ x:T.~(t~x)~\not\triangleright_η~t
-
-   This is because, in general, the type of :math:`t` need not to be convertible
-   to the type of :math:`λ x:T.~(t~x)`. E.g., if we take :math:`f` such that:
-
-   .. math::
-      f ~:~ ∀ x:\Type(2),~\Type(1)
-
-   then
-
-   .. math::
-      λ x:\Type(1).~(f~x) ~:~ ∀ x:\Type(1),~\Type(1)
-
-   We could not allow
-
-   .. math::
-      λ x:\Type(1).~(f~x) ~\triangleright_η~ f
-
-   because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be
-   convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`.
-
-.. _proof-irrelevance:
-
-Proof Irrelevance
-~~~~~~~~~~~~~~~~~
-
-It is legal to identify any two terms whose common type is a strict
-proposition :math:`A : \SProp`. Terms in a strict propositions are
-therefore called *irrelevant*.
-
-.. _convertibility:
-
-Convertibility
-~~~~~~~~~~~~~~
-
-Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the
-relation :math:`t` reduces to :math:`u` in the global environment
-:math:`E` and local context :math:`Γ` with one of the previous
-reductions β, δ, ι or ζ.
-
-We say that two terms :math:`t_1` and :math:`t_2` are
-*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the
-global environment :math:`E` and local context :math:`Γ` iff there
-exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright
-… \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and
-:math:`u_2` are identical up to irrelevant subterms, or they are convertible up to η-expansion,
-i.e. :math:`u_1` is :math:`λ x:T.~u_1'` and :math:`u_2 x` is
-recursively convertible to :math:`u_1'`, or, symmetrically,
-:math:`u_2` is :math:`λx:T.~u_2'`
-and :math:`u_1 x` is recursively convertible to :math:`u_2'`. We then write
-:math:`E[Γ] ⊢ t_1 =_{βδιζη} t_2`.
-
-Apart from this we consider two instances of polymorphic and
-cumulative (see Chapter :ref:`polymorphicuniverses`) inductive types
-(see below) convertible
-
-.. math::
-   E[Γ] ⊢ t~w_1 … w_m =_{βδιζη} t~w_1' … w_m'
-
-if we have subtypings (see below) in both directions, i.e.,
-
-.. math::
-   E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t~w_1' … w_m'
-
-and
-
-.. math::
-   E[Γ] ⊢ t~w_1' … w_m' ≤_{βδιζη} t~w_1 … w_m.
-
-Furthermore, we consider
-
-.. math::
-   E[Γ] ⊢ c~v_1 … v_m =_{βδιζη} c'~v_1' … v_m'
-
-convertible if
-
-.. math::
-   E[Γ] ⊢ v_i =_{βδιζη} v_i'
-
-and we have that :math:`c` and :math:`c'`
-are the same constructors of different instances of the same inductive
-types (differing only in universe levels) such that
-
-.. math::
-   E[Γ] ⊢ c~v_1 … v_m : t~w_1 … w_m
-
-and
-
-.. math::
-   E[Γ] ⊢ c'~v_1' … v_m' : t'~ w_1' … w_m '
-
-and we have
-
-.. math::
-   E[Γ] ⊢ t~w_1 … w_m =_{βδιζη} t~w_1' … w_m'.
-
-The convertibility relation allows introducing a new typing rule which
-says that two convertible well-formed types have the same inhabitants.
-
-
 .. _subtyping-rules:
 
 Subtyping rules
@@ -728,1219 +421,6 @@ normal form must not be confused with the normal form since some :math:`u_i`
 can be reducible. Similar notions of head-normal forms involving δ, ι
 and ζ reductions or any combination of those can also be defined.
 
-
-.. _inductive-definitions:
-
-Inductive Definitions
--------------------------
-
-Formally, we can represent any *inductive definition* as
-:math:`\ind{p}{Γ_I}{Γ_C}` where:
-
-+ :math:`Γ_I` determines the names and types of inductive types;
-+ :math:`Γ_C` determines the names and types of constructors of these
-  inductive types;
-+ :math:`p` determines the number of parameters of these inductive types.
-
-
-These inductive definitions, together with global assumptions and
-global definitions, then form the global environment. Additionally,
-for any :math:`p` there always exists :math:`Γ_P =[a_1 :A_1 ;~…;~a_p :A_p ]` such that
-each :math:`T` in :math:`(t:T)∈Γ_I \cup Γ_C` can be written as: :math:`∀Γ_P , T'` where :math:`Γ_P` is
-called the *context of parameters*. Furthermore, we must have that
-each :math:`T` in :math:`(t:T)∈Γ_I` can be written as: :math:`∀Γ_P,∀Γ_{\mathit{Arr}(t)}, S` where
-:math:`Γ_{\mathit{Arr}(t)}` is called the *Arity* of the inductive type :math:`t` and :math:`S` is called
-the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` which is the set of sorts).
-
-.. example::
-
-   The declaration for parameterized lists is:
-
-   .. math::
-      \ind{1}{[\List:\Set→\Set]}{\left[\begin{array}{rcl}
-      \Nil & : & ∀ A:\Set,~\List~A \\
-      \cons & : & ∀ A:\Set,~A→ \List~A→ \List~A
-      \end{array}
-      \right]}
-
-   which corresponds to the result of the |Coq| declaration:
-
-   .. coqtop:: in
-
-      Inductive list (A:Set) : Set :=
-      | nil : list A
-      | cons : A -> list A -> list A.
-
-.. example::
-
-   The declaration for a mutual inductive definition of tree and forest
-   is:
-
-   .. math::
-      \ind{0}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]}
-       {\left[\begin{array}{rcl}
-                \node &:& \forest → \tree\\
-                \emptyf &:& \forest\\
-                \consf &:& \tree → \forest → \forest\\
-                          \end{array}\right]}
-
-   which corresponds to the result of the |Coq| declaration:
-
-   .. coqtop:: in
-
-      Inductive tree : Set :=
-      | node : forest -> tree
-      with forest : Set :=
-      | emptyf : forest
-      | consf : tree -> forest -> forest.
-
-.. example::
-
-   The declaration for a mutual inductive definition of even and odd is:
-
-   .. math::
-      \ind{0}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\
-                                      \odd&:&\nat → \Prop \end{array}\right]}
-       {\left[\begin{array}{rcl}
-                \evenO &:& \even~0\\
-                \evenS &:& ∀ n,~\odd~n → \even~(\nS~n)\\
-                \oddS &:& ∀ n,~\even~n → \odd~(\nS~n)
-                          \end{array}\right]}
-
-   which corresponds to the result of the |Coq| declaration:
-
-   .. coqtop:: in
-
-      Inductive even : nat -> Prop :=
-      | even_O : even 0
-      | even_S : forall n, odd n -> even (S n)
-      with odd : nat -> Prop :=
-      | odd_S : forall n, even n -> odd (S n).
-
-
-
-.. _Types-of-inductive-objects:
-
-Types of inductive objects
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-We have to give the type of constants in a global environment :math:`E` which
-contains an inductive definition.
-
-.. inference:: Ind
-
-   \WFE{Γ}
-   \ind{p}{Γ_I}{Γ_C} ∈ E
-   (a:A)∈Γ_I
-   ---------------------
-   E[Γ] ⊢ a : A
-
-.. inference:: Constr
-
-   \WFE{Γ}
-   \ind{p}{Γ_I}{Γ_C} ∈ E
-   (c:C)∈Γ_C
-   ---------------------
-   E[Γ] ⊢ c : C
-
-.. example::
-
-   Provided that our environment :math:`E` contains inductive definitions we showed before,
-   these two inference rules above enable us to conclude that:
-
-   .. math::
-      \begin{array}{l}
-      E[Γ] ⊢ \even : \nat→\Prop\\
-      E[Γ] ⊢ \odd : \nat→\Prop\\
-      E[Γ] ⊢ \evenO : \even~\nO\\
-      E[Γ] ⊢ \evenS : ∀ n:\nat,~\odd~n → \even~(\nS~n)\\
-      E[Γ] ⊢ \oddS : ∀ n:\nat,~\even~n → \odd~(\nS~n)
-      \end{array}
-
-
-
-
-.. _Well-formed-inductive-definitions:
-
-Well-formed inductive definitions
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-We cannot accept any inductive definition because some of them lead
-to inconsistent systems. We restrict ourselves to definitions which
-satisfy a syntactic criterion of positivity. Before giving the formal
-rules, we need a few definitions:
-
-Arity of a given sort
-+++++++++++++++++++++
-
-A type :math:`T` is an *arity of sort* :math:`s` if it converts to the sort :math:`s` or to a
-product :math:`∀ x:T,~U` with :math:`U` an arity of sort :math:`s`.
-
-.. example::
-
-   :math:`A→\Set` is an arity of sort :math:`\Set`. :math:`∀ A:\Prop,~A→ \Prop` is an arity of sort
-   :math:`\Prop`.
-
-
-Arity
-+++++
-A type :math:`T` is an *arity* if there is a :math:`s∈ \Sort` such that :math:`T` is an arity of
-sort :math:`s`.
-
-
-.. example::
-
-   :math:`A→ \Set` and :math:`∀ A:\Prop,~A→ \Prop` are arities.
-
-
-Type of constructor
-+++++++++++++++++++
-We say that :math:`T` is a *type of constructor of* :math:`I` in one of the following
-two cases:
-
-+ :math:`T` is :math:`(I~t_1 … t_n )`
-+ :math:`T` is :math:`∀ x:U,~T'` where :math:`T'` is also a type of constructor of :math:`I`
-
-.. example::
-
-   :math:`\nat` and :math:`\nat→\nat` are types of constructor of :math:`\nat`.
-   :math:`∀ A:\Type,~\List~A` and :math:`∀ A:\Type,~A→\List~A→\List~A` are types of constructor of :math:`\List`.
-
-.. _positivity:
-
-Positivity Condition
-++++++++++++++++++++
-
-The type of constructor :math:`T` will be said to *satisfy the positivity
-condition* for a constant :math:`X` in the following cases:
-
-+ :math:`T=(X~t_1 … t_n )` and :math:`X` does not occur free in any :math:`t_i`
-+ :math:`T=∀ x:U,~V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V`
-  satisfies the positivity condition for :math:`X`.
-
-Strict positivity
-+++++++++++++++++
-
-The constant :math:`X` *occurs strictly positively* in :math:`T` in the following
-cases:
-
-
-+ :math:`X` does not occur in :math:`T`
-+ :math:`T` converts to :math:`(X~t_1 … t_n )` and :math:`X` does not occur in any of :math:`t_i`
-+ :math:`T` converts to :math:`∀ x:U,~V` and :math:`X` does not occur in type :math:`U` but occurs
-  strictly positively in type :math:`V`
-+ :math:`T` converts to :math:`(I~a_1 … a_m~t_1 … t_p )` where :math:`I` is the name of an
-  inductive definition of the form
-
-  .. math::
-     \ind{m}{I:A}{c_1 :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_1 ;~…;~c_n :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_n}
-
-  (in particular, it is
-  not mutually defined and it has :math:`m` parameters) and :math:`X` does not occur in
-  any of the :math:`t_i`, and the (instantiated) types of constructor
-  :math:`\subst{C_i}{p_j}{a_j}_{j=1… m}` of :math:`I` satisfy the nested positivity condition for :math:`X`
-
-Nested Positivity
-+++++++++++++++++
-
-The type of constructor :math:`T` of :math:`I` *satisfies the nested positivity
-condition* for a constant :math:`X` in the following cases:
-
-+ :math:`T=(I~b_1 … b_m~u_1 … u_p)`, :math:`I` is an inductive type with :math:`m`
-  parameters and :math:`X` does not occur in any :math:`u_i`
-+ :math:`T=∀ x:U,~V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V`
-  satisfies the nested positivity condition for :math:`X`
-
-
-.. example::
-
-   For instance, if one considers the following variant of a tree type
-   branching over the natural numbers:
-
-   .. coqtop:: in
-
-      Inductive nattree (A:Type) : Type :=
-      | leaf : nattree A
-      | natnode : A -> (nat -> nattree A) -> nattree A.
-
-   Then every instantiated constructor of ``nattree A`` satisfies the nested positivity
-   condition for ``nattree``:
-
-   + Type ``nattree A`` of constructor ``leaf`` satisfies the positivity condition for
-     ``nattree`` because ``nattree`` does not appear in any (real) arguments of the
-     type of that constructor (primarily because ``nattree`` does not have any (real)
-     arguments) ... (bullet 1)
-
-   + Type ``A → (nat → nattree A) → nattree A`` of constructor ``natnode`` satisfies the
-     positivity condition for ``nattree`` because:
-
-     - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 1)
-
-     - ``nattree`` occurs only strictly positively in ``nat → nattree A`` ... (bullet 3 + 2)
-
-     - ``nattree`` satisfies the positivity condition for ``nattree A`` ... (bullet 1)
-
-.. _Correctness-rules:
-
-Correctness rules
-+++++++++++++++++
-
-We shall now describe the rules allowing the introduction of a new
-inductive definition.
-
-Let :math:`E` be a global environment and :math:`Γ_P`, :math:`Γ_I`, :math:`Γ_C` be contexts
-such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k]`, and
-:math:`Γ_C` is :math:`[c_1:∀ Γ_P ,C_1 ;~…;~c_n :∀ Γ_P ,C_n ]`. Then
-
-.. inference:: W-Ind
-
-   \WFE{Γ_P}
-   (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n}
-   ------------------------------------------
-   \WF{E;~\ind{p}{Γ_I}{Γ_C}}{}
-
-
-provided that the following side conditions hold:
-
-    + :math:`k>0` and all of :math:`I_j` and :math:`c_i` are distinct names for :math:`j=1… k` and :math:`i=1… n`,
-    + :math:`p` is the number of parameters of :math:`\ind{p}{Γ_I}{Γ_C}` and :math:`Γ_P` is the
-      context of parameters,
-    + for :math:`j=1… k` we have that :math:`A_j` is an arity of sort :math:`s_j` and :math:`I_j ∉ E`,
-    + for :math:`i=1… n` we have that :math:`C_i` is a type of constructor of :math:`I_{q_i}` which
-      satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉  E`.
-
-One can remark that there is a constraint between the sort of the
-arity of the inductive type and the sort of the type of its
-constructors which will always be satisfied for the impredicative
-sorts :math:`\SProp` and :math:`\Prop` but may fail to define
-inductive type on sort :math:`\Set` and generate constraints
-between universes for inductive types in the Type hierarchy.
-
-
-.. example::
-
-   It is well known that the existential quantifier can be encoded as an
-   inductive definition. The following declaration introduces the
-   second-order existential quantifier :math:`∃ X.P(X)`.
-
-   .. coqtop:: in
-
-      Inductive exProp (P:Prop->Prop) : Prop :=
-      | exP_intro : forall X:Prop, P X -> exProp P.
-
-   The same definition on :math:`\Set` is not allowed and fails:
-
-   .. coqtop:: all
-
-      Fail Inductive exSet (P:Set->Prop) : Set :=
-      exS_intro : forall X:Set, P X -> exSet P.
-
-   It is possible to declare the same inductive definition in the
-   universe :math:`\Type`. The :g:`exType` inductive definition has type
-   :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT}_{\kw{intro}}`
-   has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`.
-
-   .. coqtop:: all
-
-      Inductive exType (P:Type->Prop) : Type :=
-      exT_intro : forall X:Type, P X -> exType P.
-
-
-.. example:: Negative occurrence (first example)
-
-   The following inductive definition is rejected because it does not
-   satisfy the positivity condition:
-
-   .. coqtop:: all
-
-      Fail Inductive I : Prop := not_I_I (not_I : I -> False) : I.
-
-   If we were to accept such definition, we could derive a
-   contradiction from it (we can test this by disabling the
-   :flag:`Positivity Checking` flag):
-
-   .. coqtop:: none
-
-      Unset Positivity Checking.
-      Inductive I : Prop := not_I_I (not_I : I -> False) : I.
-      Set Positivity Checking.
-
-   .. coqtop:: all
-
-      Definition I_not_I : I -> ~ I := fun i =>
-        match i with not_I_I not_I => not_I end.
-
-   .. coqtop:: in
-
-      Lemma contradiction : False.
-      Proof.
-        enough (I /\ ~ I) as [] by contradiction.
-        split.
-        - apply not_I_I.
-          intro.
-          now apply I_not_I.
-        - intro.
-          now apply I_not_I.
-      Qed.
-
-.. example:: Negative occurrence (second example)
-
-   Here is another example of an inductive definition which is
-   rejected because it does not satify the positivity condition:
-
-   .. coqtop:: all
-
-      Fail Inductive Lam := lam (_ : Lam -> Lam).
-
-   Again, if we were to accept it, we could derive a contradiction
-   (this time through a non-terminating recursive function):
-
-   .. coqtop:: none
-
-      Unset Positivity Checking.
-      Inductive Lam := lam (_ : Lam -> Lam).
-      Set Positivity Checking.
-
-   .. coqtop:: all
-
-      Fixpoint infinite_loop l : False :=
-        match l with lam x => infinite_loop (x l) end.
-
-      Check infinite_loop (lam (@id Lam)) : False.
-
-.. example:: Non strictly positive occurrence
-
-   It is less obvious why inductive type definitions with occurences
-   that are positive but not strictly positive are harmful.
-   We will see that in presence of an impredicative type they
-   are unsound:
-
-   .. coqtop:: all
-
-      Fail Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
-
-   If we were to accept this definition we could derive a contradiction
-   by creating an injective function from :math:`A → \Prop` to :math:`A`.
-
-   This function is defined by composing the injective constructor of
-   the type :math:`A` with the function :math:`λx. λz. z = x` injecting
-   any type :math:`T` into :math:`T → \Prop`.
-
-   .. coqtop:: none
-
-      Unset Positivity Checking.
-      Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
-      Set Positivity Checking.
-
-   .. coqtop:: all
-
-      Definition f (x: A -> Prop): A := introA (fun z => z = x).
-
-   .. coqtop:: in
-
-      Lemma f_inj: forall x y, f x = f y -> x = y.
-      Proof.
-        unfold f; intros ? ? H; injection H.
-        set (F := fun z => z = y); intro HF.
-        symmetry; replace (y = x) with (F y).
-        + unfold F; reflexivity.
-        + rewrite <- HF; reflexivity.
-      Qed.
-
-   The type :math:`A → \Prop` can be understood as the powerset
-   of the type :math:`A`. To derive a contradiction from the
-   injective function :math:`f` we use Cantor's classic diagonal
-   argument.
-
-   .. coqtop:: all
-
-      Definition d: A -> Prop := fun x => exists s, x = f s /\ ~s x.
-      Definition fd: A := f d.
-
-   .. coqtop:: in
-
-      Lemma cantor: (d fd) <-> ~(d fd).
-      Proof.
-        split.
-        + intros [s [H1 H2]]; unfold fd in H1.
-          replace d with s.
-          * assumption.
-          * apply f_inj; congruence.
-        + intro; exists d; tauto.
-      Qed.
-
-      Lemma bad: False.
-      Proof.
-        pose cantor; tauto.
-      Qed.
-
-   This derivation was first presented by Thierry Coquand and Christine
-   Paulin in :cite:`CP90`.
-
-.. _Template-polymorphism:
-
-Template polymorphism
-+++++++++++++++++++++
-
-Inductive types can be made polymorphic over the universes introduced by
-their parameters in :math:`\Type`, if the minimal inferred sort of the
-inductive declarations either mention some of those parameter universes
-or is computed to be :math:`\Prop` or :math:`\Set`.
-
-If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}`
-for the arity obtained from :math:`A` by replacing its sort with :math:`s`.
-Especially, if :math:`A` is well-typed in some global environment and local
-context, then :math:`A_{/s}` is typable by typability of all products in the
-Calculus of Inductive Constructions. The following typing rule is
-added to the theory.
-
-Let :math:`\ind{p}{Γ_I}{Γ_C}` be an inductive definition. Let
-:math:`Γ_P = [p_1 :P_1 ;~…;~p_p :P_p ]` be its context of parameters,
-:math:`Γ_I = [I_1:∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k ]` its context of definitions and
-:math:`Γ_C = [c_1 :∀ Γ_P ,C_1 ;~…;~c_n :∀ Γ_P ,C_n]` its context of constructors,
-with :math:`c_i` a constructor of :math:`I_{q_i}`. Let :math:`m ≤ p` be the length of the
-longest prefix of parameters such that the :math:`m` first arguments of all
-occurrences of all :math:`I_j` in all :math:`C_k` (even the occurrences in the
-hypotheses of :math:`C_k`) are exactly applied to :math:`p_1 … p_m` (:math:`m` is the number
-of *recursively uniform parameters* and the :math:`p−m` remaining parameters
-are the *recursively non-uniform parameters*). Let :math:`q_1 , …, q_r`, with
-:math:`0≤ r≤ m`, be a (possibly) partial instantiation of the recursively
-uniform parameters of :math:`Γ_P`. We have:
-
-.. inference:: Ind-Family
-
-   \left\{\begin{array}{l}
-   \ind{p}{Γ_I}{Γ_C} \in E\\
-   (E[]  ⊢ q_l : P'_l)_{l=1\ldots r}\\
-   (E[]  ⊢ P'_l ≤_{βδιζη} \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1})_{l=1\ldots r}\\
-   1 \leq j \leq k
-   \end{array}
-   \right.
-   -----------------------------
-   E[] ⊢ I_j~q_1 … q_r :∀ [p_{r+1} :P_{r+1} ;~…;~p_p :P_p], (A_j)_{/s_j}
-
-provided that the following side conditions hold:
-
-    + :math:`Γ_{P′}` is the context obtained from :math:`Γ_P` by replacing each :math:`P_l` that is
-      an arity with :math:`P_l'` for :math:`1≤ l ≤ r` (notice that :math:`P_l` arity implies :math:`P_l'`
-      arity since :math:`E[] ⊢ P_l' ≤_{βδιζη} \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}`);
-    + there are sorts :math:`s_i`, for :math:`1 ≤ i ≤ k` such that, for
-      :math:`Γ_{I'} = [I_1 :∀ Γ_{P'} ,(A_1)_{/s_1} ;~…;~I_k :∀ Γ_{P'} ,(A_k)_{/s_k}]`
-      we have :math:`(E[Γ_{I′} ;Γ_{P′}] ⊢ C_i : s_{q_i})_{i=1… n}` ;
-    + the sorts :math:`s_i` are all introduced by the inductive
-      declaration and have no universe constraints beside being greater
-      than or equal to :math:`\Prop`, and such that all
-      eliminations, to :math:`\Prop`, :math:`\Set` and :math:`\Type(j)`,
-      are allowed (see Section :ref:`Destructors`).
-
-
-Notice that if :math:`I_j~q_1 … q_r` is typable using the rules **Ind-Const** and
-**App**, then it is typable using the rule **Ind-Family**. Conversely, the
-extended theory is not stronger than the theory without **Ind-Family**. We
-get an equiconsistency result by mapping each :math:`\ind{p}{Γ_I}{Γ_C}`
-occurring into a given derivation into as many different inductive
-types and constructors as the number of different (partial)
-replacements of sorts, needed for this derivation, in the parameters
-that are arities (this is possible because :math:`\ind{p}{Γ_I}{Γ_C}` well-formed
-implies that :math:`\ind{p}{Γ_{I'}}{Γ_{C'}}` is well-formed and has the
-same allowed eliminations, where :math:`Γ_{I′}` is defined as above and
-:math:`Γ_{C′} = [c_1 :∀ Γ_{P′} ,C_1 ;~…;~c_n :∀ Γ_{P′} ,C_n ]`). That is, the changes in the
-types of each partial instance :math:`q_1 … q_r` can be characterized by the
-ordered sets of arity sorts among the types of parameters, and to each
-signature is associated a new inductive definition with fresh names.
-Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
-:math:`C_i~q_1 … q_r` is mapped to the names chosen in the specific instance of
-:math:`\ind{p}{Γ_I}{Γ_C}`.
-
-.. warning::
-
-   The restriction that sorts are introduced by the inductive
-   declaration prevents inductive types declared in sections to be
-   template-polymorphic on universes introduced previously in the
-   section: they cannot parameterize over the universes introduced with
-   section variables that become parameters at section closing time, as
-   these may be shared with other definitions from the same section
-   which can impose constraints on them.
-
-.. flag:: Auto Template Polymorphism
-
-   This flag, enabled by default, makes every inductive type declared
-   at level :math:`\Type` (without annotations or hiding it behind a
-   definition) template polymorphic if possible.
-
-   This can be prevented using the :attr:`universes(notemplate)`
-   attribute.
-
-   Template polymorphism and full universe polymorphism (see Chapter
-   :ref:`polymorphicuniverses`) are incompatible, so if the latter is
-   enabled (through the :flag:`Universe Polymorphism` flag or the
-   :attr:`universes(polymorphic)` attribute) it will prevail over
-   automatic template polymorphism.
-
-.. warn:: Automatically declaring @ident as template polymorphic.
-
-   Warning ``auto-template`` can be used (it is off by default) to
-   find which types are implicitly declared template polymorphic by
-   :flag:`Auto Template Polymorphism`.
-
-   An inductive type can be forced to be template polymorphic using
-   the :attr:`universes(template)` attribute: in this case, the
-   warning is not emitted.
-
-.. attr:: universes(template)
-
-   This attribute can be used to explicitly declare an inductive type
-   as template polymorphic, whether the :flag:`Auto Template
-   Polymorphism` flag is on or off.
-
-   .. exn:: template and polymorphism not compatible
-
-      This attribute cannot be used in a full universe polymorphic
-      context, i.e. if the :flag:`Universe Polymorphism` flag is on or
-      if the :attr:`universes(polymorphic)` attribute is used.
-
-   .. exn:: Ill-formed template inductive declaration: not polymorphic on any universe.
-
-      The attribute was used but the inductive definition does not
-      satisfy the criterion to be template polymorphic.
-
-.. attr:: universes(notemplate)
-
-   This attribute can be used to prevent an inductive type to be
-   template polymorphic, even if the :flag:`Auto Template
-   Polymorphism` flag is on.
-
-In practice, the rule **Ind-Family** is used by |Coq| only when all the
-inductive types of the inductive definition are declared with an arity
-whose sort is in the Type hierarchy. Then, the polymorphism is over
-the parameters whose type is an arity of sort in the Type hierarchy.
-The sorts :math:`s_j` are chosen canonically so that each :math:`s_j` is minimal with
-respect to the hierarchy :math:`\Prop ⊂ \Set_p ⊂ \Type` where :math:`\Set_p` is predicative
-:math:`\Set`. More precisely, an empty or small singleton inductive definition
-(i.e. an inductive definition of which all inductive types are
-singleton – see Section :ref:`Destructors`) is set in :math:`\Prop`, a small non-singleton
-inductive type is set in :math:`\Set` (even in case :math:`\Set` is impredicative – see
-Section The-Calculus-of-Inductive-Construction-with-impredicative-Set_),
-and otherwise in the Type hierarchy.
-
-Note that the side-condition about allowed elimination sorts in the rule
-**Ind-Family** avoids to recompute the allowed elimination sorts at each
-instance of a pattern matching (see Section :ref:`Destructors`). As an
-example, let us consider the following definition:
-
-.. example::
-
-   .. coqtop:: in
-
-      Inductive option (A:Type) : Type :=
-      | None : option A
-      | Some : A -> option A.
-
-As the definition is set in the Type hierarchy, it is used
-polymorphically over its parameters whose types are arities of a sort
-in the Type hierarchy. Here, the parameter :math:`A` has this property, hence,
-if :g:`option` is applied to a type in :math:`\Set`, the result is in :math:`\Set`. Note that
-if :g:`option` is applied to a type in :math:`\Prop`, then, the result is not set in
-:math:`\Prop` but in :math:`\Set` still. This is because :g:`option` is not a singleton type
-(see Section :ref:`Destructors`) and it would lose the elimination to :math:`\Set` and :math:`\Type`
-if set in :math:`\Prop`.
-
-.. example::
-
-   .. coqtop:: all
-
-      Check (fun A:Set => option A).
-      Check (fun A:Prop => option A).
-
-Here is another example.
-
-.. example::
-
-   .. coqtop:: in
-
-      Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
-
-As :g:`prod` is a singleton type, it will be in :math:`\Prop` if applied twice to
-propositions, in :math:`\Set` if applied twice to at least one type in :math:`\Set` and
-none in :math:`\Type`, and in :math:`\Type` otherwise. In all cases, the three kind of
-eliminations schemes are allowed.
-
-.. example::
-
-   .. coqtop:: all
-
-      Check (fun A:Set => prod A).
-      Check (fun A:Prop => prod A A).
-      Check (fun (A:Prop) (B:Set) => prod A B).
-      Check (fun (A:Type) (B:Prop) => prod A B).
-
-.. note::
-   Template polymorphism used to be called “sort-polymorphism of
-   inductive types” before universe polymorphism
-   (see Chapter :ref:`polymorphicuniverses`) was introduced.
-
-
-.. _Destructors:
-
-Destructors
-~~~~~~~~~~~~~~~~~
-
-The specification of inductive definitions with arities and
-constructors is quite natural. But we still have to say how to use an
-object in an inductive type.
-
-This problem is rather delicate. There are actually several different
-ways to do that. Some of them are logically equivalent but not always
-equivalent from the computational point of view or from the user point
-of view.
-
-From the computational point of view, we want to be able to define a
-function whose domain is an inductively defined type by using a
-combination of case analysis over the possible constructors of the
-object and recursion.
-
-Because we need to keep a consistent theory and also we prefer to keep
-a strongly normalizing reduction, we cannot accept any sort of
-recursion (even terminating). So the basic idea is to restrict
-ourselves to primitive recursive functions and functionals.
-
-For instance, assuming a parameter :math:`A:\Set` exists in the local context,
-we want to build a function :math:`\length` of type :math:`\List~A → \nat` which computes
-the length of the list, such that :math:`(\length~(\Nil~A)) = \nO` and
-:math:`(\length~(\cons~A~a~l)) = (\nS~(\length~l))`.
-We want these equalities to be
-recognized implicitly and taken into account in the conversion rule.
-
-From the logical point of view, we have built a type family by giving
-a set of constructors. We want to capture the fact that we do not have
-any other way to build an object in this type. So when trying to prove
-a property about an object :math:`m` in an inductive type it is enough
-to enumerate all the cases where :math:`m` starts with a different
-constructor.
-
-In case the inductive definition is effectively a recursive one, we
-want to capture the extra property that we have built the smallest
-fixed point of this recursive equation. This says that we are only
-manipulating finite objects. This analysis provides induction
-principles. For instance, in order to prove
-:math:`∀ l:\List~A,~(\kw{has}\_\kw{length}~A~l~(\length~l))` it is enough to prove:
-
-
-+ :math:`(\kw{has}\_\kw{length}~A~(\Nil~A)~(\length~(\Nil~A)))`
-+ :math:`∀ a:A,~∀ l:\List~A,~(\kw{has}\_\kw{length}~A~l~(\length~l)) →`
-  :math:`(\kw{has}\_\kw{length}~A~(\cons~A~a~l)~(\length~(\cons~A~a~l)))`
-
-
-which given the conversion equalities satisfied by :math:`\length` is the same
-as proving:
-
-
-+ :math:`(\kw{has}\_\kw{length}~A~(\Nil~A)~\nO)`
-+ :math:`∀ a:A,~∀ l:\List~A,~(\kw{has}\_\kw{length}~A~l~(\length~l)) →`
-  :math:`(\kw{has}\_\kw{length}~A~(\cons~A~a~l)~(\nS~(\length~l)))`
-
-
-One conceptually simple way to do that, following the basic scheme
-proposed by Martin-Löf in his Intuitionistic Type Theory, is to
-introduce for each inductive definition an elimination operator. At
-the logical level it is a proof of the usual induction principle and
-at the computational level it implements a generic operator for doing
-primitive recursion over the structure.
-
-But this operator is rather tedious to implement and use. We choose in
-this version of |Coq| to factorize the operator for primitive recursion
-into two more primitive operations as was first suggested by Th.
-Coquand in :cite:`Coq92`. One is the definition by pattern matching. The
-second one is a definition by guarded fixpoints.
-
-
-.. _match-construction:
-
-The match ... with ... end construction
-+++++++++++++++++++++++++++++++++++++++
-
-The basic idea of this operator is that we have an object :math:`m` in an
-inductive type :math:`I` and we want to prove a property which possibly
-depends on :math:`m`. For this, it is enough to prove the property for
-:math:`m = (c_i~u_1 … u_{p_i} )` for each constructor of :math:`I`.
-The |Coq| term for this proof
-will be written:
-
-.. math::
-   \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend
-
-In this expression, if :math:`m` eventually happens to evaluate to
-:math:`(c_i~u_1 … u_{p_i})` then the expression will behave as specified in its :math:`i`-th branch
-and it will reduce to :math:`f_i` where the :math:`x_{i1} …x_{ip_i}` are replaced by the
-:math:`u_1 … u_{p_i}` according to the ι-reduction.
-
-Actually, for type checking a :math:`\Match…\with…\kwend` expression we also need
-to know the predicate :math:`P` to be proved by case analysis. In the general
-case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate
-over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I`
-(parameters excluded), and the last one corresponds to object :math:`m`. |Coq|
-can sometimes infer this predicate but sometimes not. The concrete
-syntax for describing this predicate uses the :math:`\as…\In…\return`
-construction. For instance, let us assume that :math:`I` is an unary predicate
-with one parameter and one argument. The predicate is made explicit
-using the syntax:
-
-.. math::
-   \Match~m~\as~x~\In~I~\_~a~\return~P~\with~
-   (c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | …
-   | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend
-
-The :math:`\as` part can be omitted if either the result type does not depend
-on :math:`m` (non-dependent elimination) or :math:`m` is a variable (in this case, :math:`m`
-can occur in :math:`P` where it is considered a bound variable). The :math:`\In` part
-can be omitted if the result type does not depend on the arguments
-of :math:`I`. Note that the arguments of :math:`I` corresponding to parameters *must*
-be :math:`\_`, because the result type is not generalized to all possible
-values of the parameters. The other arguments of :math:`I` (sometimes called
-indices in the literature) have to be variables (:math:`a` above) and these
-variables can occur in :math:`P`. The expression after :math:`\In` must be seen as an
-*inductive type pattern*. Notice that expansion of implicit arguments
-and notations apply to this pattern. For the purpose of presenting the
-inference rules, we use a more compact notation:
-
-.. math::
-   \case(m,(λ a x . P), λ x_{11} ... x_{1p_1} . f_1~| … |~λ x_{n1} ...x_{np_n} . f_n )
-
-
-.. _Allowed-elimination-sorts:
-
-**Allowed elimination sorts.** An important question for building the typing rule for :math:`\Match` is what
-can be the type of :math:`λ a x . P` with respect to the type of :math:`m`. If :math:`m:I`
-and :math:`I:A` and :math:`λ a x . P : B` then by :math:`[I:A|B]` we mean that one can use
-:math:`λ a x . P` with :math:`m` in the above match-construct.
-
-
-.. _cic_notations:
-
-**Notations.** The :math:`[I:A|B]` is defined as the smallest relation satisfying the
-following rules: We write :math:`[I|B]` for :math:`[I:A|B]` where :math:`A` is the type of :math:`I`.
-
-The case of inductive types in sorts :math:`\Set` or :math:`\Type` is simple.
-There is no restriction on the sort of the predicate to be eliminated.
-
-.. inference:: Prod
-
-   [(I~x):A′|B′]
-   -----------------------
-   [I:∀ x:A,~A′|∀ x:A,~B′]
-
-
-.. inference:: Set & Type
-
-   s_1 ∈ \{\Set,\Type(j)\}
-   s_2 ∈ \Sort
-   ----------------
-   [I:s_1 |I→ s_2 ]
-
-
-The case of Inductive definitions of sort :math:`\Prop` is a bit more
-complicated, because of our interpretation of this sort. The only
-harmless allowed eliminations, are the ones when predicate :math:`P`
-is also of sort :math:`\Prop` or is of the morally smaller sort
-:math:`\SProp`.
-
-.. inference:: Prop
-
-   s ∈ \{\SProp,\Prop\}
-   --------------------
-   [I:\Prop|I→s]
-
-
-:math:`\Prop` is the type of logical propositions, the proofs of properties :math:`P` in
-:math:`\Prop` could not be used for computation and are consequently ignored by
-the extraction mechanism. Assume :math:`A` and :math:`B` are two propositions, and the
-logical disjunction :math:`A ∨ B` is defined inductively by:
-
-.. example::
-
-   .. coqtop:: in
-
-      Inductive or (A B:Prop) : Prop :=
-      or_introl : A -> or A B | or_intror : B -> or A B.
-
-
-The following definition which computes a boolean value by case over
-the proof of :g:`or A B` is not accepted:
-
-.. example::
-
-   .. coqtop:: all
-
-      Fail Definition choice (A B: Prop) (x:or A B) :=
-      match x with or_introl _ _ a => true | or_intror _ _ b => false end.
-
-From the computational point of view, the structure of the proof of
-:g:`(or A B)` in this term is needed for computing the boolean value.
-
-In general, if :math:`I` has type :math:`\Prop` then :math:`P` cannot have type :math:`I→\Set`, because
-it will mean to build an informative proof of type :math:`(P~m)` doing a case
-analysis over a non-computational object that will disappear in the
-extracted program. But the other way is safe with respect to our
-interpretation we can have :math:`I` a computational object and :math:`P` a
-non-computational one, it just corresponds to proving a logical property
-of a computational object.
-
-In the same spirit, elimination on :math:`P` of type :math:`I→\Type` cannot be allowed
-because it trivially implies the elimination on :math:`P` of type :math:`I→ \Set` by
-cumulativity. It also implies that there are two proofs of the same
-property which are provably different, contradicting the
-proof-irrelevance property which is sometimes a useful axiom:
-
-.. example::
-
-   .. coqtop:: all
-
-      Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
-
-The elimination of an inductive type of sort :math:`\Prop` on a predicate
-:math:`P` of type :math:`I→ \Type` leads to a paradox when applied to impredicative
-inductive definition like the second-order existential quantifier
-:g:`exProp` defined above, because it gives access to the two projections on
-this type.
-
-
-.. _Empty-and-singleton-elimination:
-
-**Empty and singleton elimination.** There are special inductive definitions in
-:math:`\Prop` for which more eliminations are allowed.
-
-.. inference:: Prop-extended
-
-   I~\kw{is an empty or singleton definition}
-   s ∈ \Sort
-   -------------------------------------
-   [I:\Prop|I→ s]
-
-A *singleton definition* has only one constructor and all the
-arguments of this constructor have type :math:`\Prop`. In that case, there is a
-canonical way to interpret the informative extraction on an object in
-that type, such that the elimination on any sort :math:`s` is legal. Typical
-examples are the conjunction of non-informative propositions and the
-equality. If there is a hypothesis :math:`h:a=b` in the local context, it can
-be used for rewriting not only in logical propositions but also in any
-type.
-
-.. example::
-
-   .. coqtop:: all
-
-      Print eq_rec.
-      Require Extraction.
-      Extraction eq_rec.
-
-An empty definition has no constructors, in that case also,
-elimination on any sort is allowed.
-
-.. _Eliminaton-for-SProp:
-
-Inductive types in :math:`\SProp` must have no constructors (i.e. be
-empty) to be eliminated to produce relevant values.
-
-Note that thanks to proof irrelevance elimination functions can be
-produced for other types, for instance the elimination for a unit type
-is the identity.
-
-.. _Type-of-branches:
-
-**Type of branches.**
-Let :math:`c` be a term of type :math:`C`, we assume :math:`C` is a type of constructor for an
-inductive type :math:`I`. Let :math:`P` be a term that represents the property to be
-proved. We assume :math:`r` is the number of parameters and :math:`s` is the number of
-arguments.
-
-We define a new type :math:`\{c:C\}^P` which represents the type of the branch
-corresponding to the :math:`c:C` constructor.
-
-.. math::
-   \begin{array}{ll}
-   \{c:(I~q_1\ldots q_r\ t_1 \ldots t_s)\}^P &\equiv (P~t_1\ldots ~t_s~c) \\
-   \{c:∀ x:T,~C\}^P &\equiv ∀ x:T,~\{(c~x):C\}^P
-   \end{array}
-
-We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:`c`.
-
-
-.. example::
-
-   The following term in concrete syntax::
-
-       match t as l return P' with
-       | nil _ => t1
-       | cons _ hd tl => t2
-       end
-
-
-   can be represented in abstract syntax as
-
-   .. math::
-      \case(t,P,f_1 | f_2 )
-
-   where
-
-   .. math::
-      :nowrap:
-
-      \begin{eqnarray*}
-        P & = & λ l.~P^\prime\\
-        f_1 & = & t_1\\
-        f_2 & = & λ (hd:\nat).~λ (tl:\List~\nat).~t_2
-      \end{eqnarray*}
-
-   According to the definition:
-
-   .. math::
-      \{(\Nil~\nat)\}^P ≡ \{(\Nil~\nat) : (\List~\nat)\}^P ≡ (P~(\Nil~\nat))
-
-   .. math::
-
-      \begin{array}{rl}
-      \{(\cons~\nat)\}^P & ≡\{(\cons~\nat) : (\nat→\List~\nat→\List~\nat)\}^P \\
-      & ≡∀ n:\nat,~\{(\cons~\nat~n) : (\List~\nat→\List~\nat)\}^P \\
-      & ≡∀ n:\nat,~∀ l:\List~\nat,~\{(\cons~\nat~n~l) : (\List~\nat)\}^P \\
-      & ≡∀ n:\nat,~∀ l:\List~\nat,~(P~(\cons~\nat~n~l)).
-      \end{array}
-
-   Given some :math:`P` then :math:`\{(\Nil~\nat)\}^P` represents the expected type of :math:`f_1`,
-   and :math:`\{(\cons~\nat)\}^P` represents the expected type of :math:`f_2`.
-
-
-.. _Typing-rule:
-
-**Typing rule.**
-Our very general destructor for inductive definition enjoys the
-following typing rule
-
-.. inference:: match
-
-   \begin{array}{l}
-   E[Γ] ⊢ c : (I~q_1 … q_r~t_1 … t_s ) \\
-   E[Γ] ⊢ P : B \\
-   [(I~q_1 … q_r)|B] \\
-   (E[Γ] ⊢ f_i : \{(c_{p_i}~q_1 … q_r)\}^P)_{i=1… l}
-   \end{array}
-   ------------------------------------------------
-   E[Γ] ⊢ \case(c,P,f_1  |… |f_l ) : (P~t_1 … t_s~c)
-
-provided :math:`I` is an inductive type in a
-definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;~…;~c_n :C_n ]` and
-:math:`c_{p_1} … c_{p_l}` are the only constructors of :math:`I`.
-
-
-
-.. example::
-
-   Below is a typing rule for the term shown in the previous example:
-
-   .. inference:: list example
-
-     \begin{array}{l}
-       E[Γ] ⊢ t : (\List ~\nat) \\
-       E[Γ] ⊢ P : B \\
-       [(\List ~\nat)|B] \\
-       E[Γ] ⊢ f_1 : \{(\Nil ~\nat)\}^P \\
-       E[Γ] ⊢ f_2 : \{(\cons ~\nat)\}^P
-     \end{array}
-     ------------------------------------------------
-     E[Γ] ⊢ \case(t,P,f_1 |f_2 ) : (P~t)
-
-
-.. _Definition-of-ι-reduction:
-
-**Definition of ι-reduction.**
-We still have to define the ι-reduction in the general case.
-
-An ι-redex is a term of the following form:
-
-.. math::
-   \case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_l )
-
-with :math:`c_{p_i}` the :math:`i`-th constructor of the inductive type :math:`I` with :math:`r`
-parameters.
-
-The ι-contraction of this term is :math:`(f_i~a_1 … a_m )` leading to the
-general reduction rule:
-
-.. math::
-   \case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_l ) \triangleright_ι (f_i~a_1 … a_m )
-
-
-.. _Fixpoint-definitions:
-
-Fixpoint definitions
-~~~~~~~~~~~~~~~~~~~~
-
-The second operator for elimination is fixpoint definition. This
-fixpoint may involve several mutually recursive definitions. The basic
-concrete syntax for a recursive set of mutually recursive declarations
-is (with :math:`Γ_i` contexts):
-
-.. math::
-   \fix~f_1 (Γ_1 ) :A_1 :=t_1~\with … \with~f_n (Γ_n ) :A_n :=t_n
-
-
-The terms are obtained by projections from this set of declarations
-and are written
-
-.. math::
-   \fix~f_1 (Γ_1 ) :A_1 :=t_1~\with … \with~f_n (Γ_n ) :A_n :=t_n~\for~f_i
-
-In the inference rules, we represent such a term by
-
-.. math::
-   \Fix~f_i\{f_1 :A_1':=t_1' … f_n :A_n':=t_n'\}
-
-with :math:`t_i'` (resp. :math:`A_i'`) representing the term :math:`t_i` abstracted (resp.
-generalized) with respect to the bindings in the context :math:`Γ_i`, namely
-:math:`t_i'=λ Γ_i . t_i` and :math:`A_i'=∀ Γ_i , A_i`.
-
-
-Typing rule
-+++++++++++
-
-The typing rule is the expected one for a fixpoint.
-
-.. inference:: Fix
-
-   (E[Γ] ⊢ A_i : s_i )_{i=1… n}
-   (E[Γ;~f_1 :A_1 ;~…;~f_n :A_n ] ⊢ t_i : A_i )_{i=1… n}
-   -------------------------------------------------------
-   E[Γ] ⊢ \Fix~f_i\{f_1 :A_1 :=t_1 … f_n :A_n :=t_n \} : A_i
-
-
-Any fixpoint definition cannot be accepted because non-normalizing
-terms allow proofs of absurdity. The basic scheme of recursion that
-should be allowed is the one needed for defining primitive recursive
-functionals. In that case the fixpoint enjoys a special syntactic
-restriction, namely one of the arguments belongs to an inductive type,
-the function starts with a case analysis and recursive calls are done
-on variables coming from patterns and representing subterms. For
-instance in the case of natural numbers, a proof of the induction
-principle of type
-
-.. math::
-   ∀ P:\nat→\Prop,~(P~\nO)→(∀ n:\nat,~(P~n)→(P~(\nS~n)))→ ∀ n:\nat,~(P~n)
-
-can be represented by the term:
-
-.. math::
-   \begin{array}{l}
-   λ P:\nat→\Prop.~λ f:(P~\nO).~λ g:(∀ n:\nat,~(P~n)→(P~(\nS~n))).\\
-   \Fix~h\{h:∀ n:\nat,~(P~n):=λ n:\nat.~\case(n,P,f | λp:\nat.~(g~p~(h~p)))\}
-   \end{array}
-
-Before accepting a fixpoint definition as being correctly typed, we
-check that the definition is “guarded”. A precise analysis of this
-notion can be found in :cite:`Gim94`. The first stage is to precise on which
-argument the fixpoint will be decreasing. The type of this argument
-should be an inductive type. For doing this, the syntax of
-fixpoints is extended and becomes
-
-.. math::
-   \Fix~f_i\{f_1/k_1 :A_1:=t_1 … f_n/k_n :A_n:=t_n\}
-
-
-where :math:`k_i` are positive integers. Each :math:`k_i` represents the index of
-parameter of :math:`f_i`, on which :math:`f_i` is decreasing. Each :math:`A_i` should be a
-type (reducible to a term) starting with at least :math:`k_i` products
-:math:`∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'` and :math:`B_{k_i}` an inductive type.
-
-Now in the definition :math:`t_i`, if :math:`f_j` occurs then it should be applied to
-at least :math:`k_j` arguments and the :math:`k_j`-th argument should be
-syntactically recognized as structurally smaller than :math:`y_{k_i}`.
-
-The definition of being structurally smaller is a bit technical. One
-needs first to define the notion of *recursive arguments of a
-constructor*. For an inductive definition :math:`\ind{r}{Γ_I}{Γ_C}`, if the
-type of a constructor :math:`c` has the form
-:math:`∀ p_1 :P_1 ,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_m :T_m,~(I_j~p_1 … p_r~t_1 … t_s )`,
-then the recursive
-arguments will correspond to :math:`T_i` in which one of the :math:`I_l` occurs.
-
-The main rules for being structurally smaller are the following.
-Given a variable :math:`y` of an inductively defined type in a declaration
-:math:`\ind{r}{Γ_I}{Γ_C}` where :math:`Γ_I` is :math:`[I_1 :A_1 ;~…;~I_k :A_k]`, and :math:`Γ_C` is
-:math:`[c_1 :C_1 ;~…;~c_n :C_n ]`, the terms structurally smaller than :math:`y` are:
-
-
-+ :math:`(t~u)` and :math:`λ x:U .~t` when :math:`t` is structurally smaller than :math:`y`.
-+ :math:`\case(c,P,f_1 … f_n)` when each :math:`f_i` is structurally smaller than :math:`y`.
-  If :math:`c` is :math:`y` or is structurally smaller than :math:`y`, its type is an inductive
-  type :math:`I_p` part of the inductive definition corresponding to :math:`y`.
-  Each :math:`f_i` corresponds to a type of constructor
-  :math:`C_q ≡ ∀ p_1 :P_1 ,~…,∀ p_r :P_r ,~∀ y_1 :B_1 ,~… ∀ y_m :B_m ,~(I_p~p_1 … p_r~t_1 … t_s )`
-  and can consequently be written :math:`λ y_1 :B_1' .~… λ y_m :B_m'.~g_i`. (:math:`B_i'` is
-  obtained from :math:`B_i` by substituting parameters for variables) the variables
-  :math:`y_j` occurring in :math:`g_i` corresponding to recursive arguments :math:`B_i` (the
-  ones in which one of the :math:`I_l` occurs) are structurally smaller than :math:`y`.
-
-
-The following definitions are correct, we enter them using the :cmd:`Fixpoint`
-command and show the internal representation.
-
-.. example::
-
-   .. coqtop:: all
-
-      Fixpoint plus (n m:nat) {struct n} : nat :=
-      match n with
-      | O => m
-      | S p => S (plus p m)
-      end.
-
-      Print plus.
-      Fixpoint lgth (A:Set) (l:list A) {struct l} : nat :=
-      match l with
-      | nil _ => O
-      | cons _ a l' => S (lgth A l')
-      end.
-      Print lgth.
-      Fixpoint sizet (t:tree) : nat := let (f) := t in S (sizef f)
-      with sizef (f:forest) : nat :=
-      match f with
-      | emptyf => O
-      | consf t f => plus (sizet t) (sizef f)
-      end.
-      Print sizet.
-
-.. _Reduction-rule:
-
-Reduction rule
-++++++++++++++
-
-Let :math:`F` be the set of declarations:
-:math:`f_1 /k_1 :A_1 :=t_1 …f_n /k_n :A_n:=t_n`.
-The reduction for fixpoints is:
-
-.. math::
-   (\Fix~f_i \{F\}~a_1 …a_{k_i}) ~\triangleright_ι~ \subst{t_i}{f_k}{\Fix~f_k \{F\}}_{k=1… n} ~a_1 … a_{k_i}
-
-when :math:`a_{k_i}` starts with a constructor. This last restriction is needed
-in order to keep strong normalization and corresponds to the reduction
-for primitive recursive operators. The following reductions are now
-possible:
-
-.. math::
-   :nowrap:
-
-   \begin{eqnarray*}
-   \plus~(\nS~(\nS~\nO))~(\nS~\nO)~& \trii & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\
-                                   & \trii & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\
-                                   & \trii & \nS~(\nS~(\nS~\nO))\\
-   \end{eqnarray*}
-
-.. _Mutual-induction:
-
-**Mutual induction**
-
-The principles of mutual induction can be automatically generated
-using the Scheme command described in Section :ref:`proofschemes-induction-principles`.
-
-
 .. _Admissible-rules-for-global-environments:
 
 Admissible rules for global environments