Correct W-Ind.

Remove the 2nd premise "(E[Γ_P ] ⊢ A_j : s_j)_(j=1...k)".
Also, "Γ" in "c_i ∉ Γ ∪ E" is changed to "Γ_I".

"E[Γ_P ] ⊢ A_j : s_j" contradicts with a side condition
"A_j is an arity of sort s_j".
The latter means that A_j is ∀ x1:T1, ... ∀ xm:Tm, s_j.
So, "(∀ x1:T1, ..., s_j) : s_j)" is required.
Using Prod-{Prop,Set,Type}, it needs "s_j : s_j" which cannot be proved.

This problem is introduced at 2018-07-22:
https://github.com/coq/coq/commit/f25c1d252ad61b4dc4321e3a11f33b1e6d4e3dff
Before that, the premise describes "A_j : s'_j".
And "s'_j" is not explained anywhere.

I think "A_j : s'_j" describes that A_j is a type (a value of a sort).
Thus, "A_j is an arity of sort s_j" imply "A_j : s'_j".

So, I removed the 2nd premise.

Also, a side condition describes "c_i ∉ Γ ∪ E" but "Γ" is not explained.
I think that Γ should be Γ_I.

Γ should include Γ_I because a constructor, c_i, and inductive types are
both defined in global environment and it cannot accept duplicate name.
Actually, such definition fails:

```
Fail Inductive X := X : X.
(* The following names are used both as type names and constructor names: X.*)
```

Γ doesn't include Γ_P because parameters are not defined in global
environment.
Actually, a parameter can be same name as a constructor name:

```
Inductive I (X : nat) := X : I X.
Check X. (* X : forall X : nat, I X *)
```

0 files changed, 0 insertions, 0 deletions