Fix index of arguments of constructor in fixpoint.

In fixpoint typing rule section, a type of constructor is described
twice:

- ∀ p_1:P_1,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_r:T_r,~(I_j~p_1 … p_r~t_1 … t_s)
- ∀ p_1:P_1,~…,∀ p_r :P_r,~∀ y_1:B_1,~… ∀ y_k:B_k,~(I~a_1 … a_k)

Both seems invalid.
The former require that the number of parameters and
the number of (non-parameter) constructor argumets is same.
The latter require that the number of (non-parameter) constructor
argumets and the number of inductive type arguments (including paramters) is
same.
Also, "k" is already used for the number of inductive types in
a inductive definition.

So, I changed the number of (non-parameter) constructor
argumets to "m".  I choose "m" because "m" is used for the purpose
in the description for iota-reduction of destructors.

Also, I changed the inductive type parameters and arguments of latter
consistent with the former.

0 files changed, 0 insertions, 0 deletions