.. some handy replacements for common items

.. role:: smallcaps

.. |A_1| replace:: `A`\ :math:`_{1}`
.. |A_n| replace:: `A`\ :math:`_{n}`
.. |arg_1| replace:: `arg`\ :math:`_{1}`
.. |arg_n| replace:: `arg`\ :math:`_{n}`
.. |bdi| replace:: :math:`\beta\delta\iota`
.. |binder_1| replace:: `binder`\ :math:`_{1}`
.. |binder_n| replace:: `binder`\ :math:`_{n}`
.. |binders_1| replace:: `binders`\ :math:`_{1}`
.. |binders_n| replace:: `binders`\ :math:`_{n}`
.. |C_1| replace:: `C`\ :math:`_{1}`
.. |c_1| replace:: `c`\ :math:`_{1}`
.. |C_2| replace:: `C`\ :math:`_{2}`
.. |c_i| replace:: `c`\ :math:`_{i}`
.. |c_n| replace:: `c`\ :math:`_{n}`
.. |Cic| replace:: :smallcaps:`Cic`
.. |class_1| replace:: `class`\ :math:`_{1}`
.. |class_2| replace:: `class`\ :math:`_{2}`
.. |Coq| replace:: :smallcaps:`Coq`
.. |CoqIDE| replace:: :smallcaps:`CoqIDE`
.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\small{\beta\delta\iota\zeta}}`
.. |Gallina| replace:: :smallcaps:`Gallina`
.. |ident_0| replace:: `ident`\ :math:`_{0}`
.. |ident_1,1| replace:: `ident`\ :math:`_{1,1}`
.. |ident_1,k_1| replace:: `ident`\ :math:`_{1,k_1}`)
.. |ident_1| replace:: `ident`\ :math:`_{1}`
.. |ident_2| replace:: `ident`\ :math:`_{2}`
.. |ident_3| replace:: `ident`\ :math:`_{3}`
.. |ident_i| replace:: `ident`\ :math:`_{i}`
.. |ident_j| replace:: `ident`\ :math:`_{j}`
.. |ident_k| replace:: `ident`\ :math:`_{k}`
.. |ident_n,1| replace:: `ident`\ :math:`_{n,1}`
.. |ident_n,k_n| replace:: `ident`\ :math:`_{n,k_n}`
.. |ident_n| replace:: `ident`\ :math:`_{n}`
.. |Latex| replace:: :smallcaps:`LaTeX`
.. |L_tac| replace:: `L`:sub:`tac`
.. |Ltac| replace:: `L`:sub:`tac`
.. |ML| replace:: :smallcaps:`ML`
.. |mod_0| replace:: `mod`\ :math:`_{0}`
.. |mod_1| replace:: `mod`\ :math:`_{1}`
.. |mod_2| replace:: `mod`\ :math:`_{1}`
.. |mod_n| replace:: `mod`\ :math:`_{n}`
.. |module_0| replace:: `module`\ :math:`_{0}`
.. |module_1| replace:: `module`\ :math:`_{1}`
.. |module_expression_0| replace:: `module_expression`\ :math:`_{0}`
.. |module_expression_1| replace:: `module_expression`\ :math:`_{1}`
.. |module_expression_i| replace:: `module_expression`\ :math:`_{i}`
.. |module_expression_n| replace:: `module_expression`\ :math:`_{n}`
.. |module_n| replace:: `module`\ :math:`_{n}`
.. |module_type_0| replace:: `module_type`\ :math:`_{0}`
.. |module_type_1| replace:: `module_type`\ :math:`_{1}`
.. |module_type_i| replace:: `module_type`\ :math:`_{i}`
.. |module_type_n| replace:: `module_type`\ :math:`_{n}`
.. |N| replace:: ``N``
.. |nat| replace:: ``nat``
.. |OCaml| replace:: :smallcaps:`OCaml`
.. |p_1| replace:: `p`\ :math:`_{1}`
.. |p_i| replace:: `p`\ :math:`_{i}`
.. |p_n| replace:: `p`\ :math:`_{n}`
.. |Program| replace:: :strong:`Program`
.. |SSR| replace:: :smallcaps:`SSReflect`
.. |t_1| replace:: `t`\ :math:`_{1}`
.. |t_i| replace:: `t`\ :math:`_{i}`
.. |t_m| replace:: `t`\ :math:`_{m}`
.. |t_n| replace:: `t`\ :math:`_{n}`
.. |f_1| replace:: `f`\ :math:`_{1}`
.. |f_i| replace:: `f`\ :math:`_{i}`
.. |f_m| replace:: `f`\ :math:`_{m}`
.. |f_n| replace:: `f`\ :math:`_{n}`
.. |u_1| replace:: `u`\ :math:`_{1}`
.. |u_i| replace:: `u`\ :math:`_{i}`
.. |u_m| replace:: `u`\ :math:`_{m}`
.. |u_n| replace:: `u`\ :math:`_{n}`
.. |term_0| replace:: `term`\ :math:`_{0}`
.. |term_1| replace:: `term`\ :math:`_{1}`
.. |term_2| replace:: `term`\ :math:`_{2}`
.. |term_n| replace:: `term`\ :math:`_{n}`
.. |type_0| replace:: `type`\ :math:`_{0}`
.. |type_1| replace:: `type`\ :math:`_{1}`
.. |type_2| replace:: `type`\ :math:`_{2}`
.. |type_3| replace:: `type`\ :math:`_{3}`
.. |type_n| replace:: `type`\ :math:`_{n}`
.. |x_1| replace:: `x`\ :math:`_{1}`
.. |x_i| replace:: `x`\ :math:`_{i}`
.. |x_n| replace:: `x`\ :math:`_{n}`
.. |Z| replace:: ``Z``