The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Dear all,

While I was trying to grok the Coq inference rules (as stated in the Coq'Art 
book), I came across this:
(pages 91,92)

        E,Γ ⊢ A : Type(i)    E,Γ ∷ (a:A) ⊢ B : Type(j)    i ≤ k    j ≤ k
   Prod ────────────────────────────────────────────────────────────────
                             E,Γ ⊢ ∀ a:A,B : Type(k)

Here I started to wonder, what are the reasons for the stated constraints:

    i ≤ k
    j ≤ k

Why (any) weaker condition, such as

    k ≤ i
    k ≤ j

, could cause problems?

I either failed to deduce it from what I know (possible),
or there is something important I do not know (likely) :-)

Thanks in advance for any help.