The Coq mailing list

[Matej Kosik <kosik AT fiit.stuba.sk>]

Hello,

I have started to read the Coq-book
(Interactive Theorem Proving and Program Development)

The general shape of the Prod(s,s',s'') rule is stated
on page 91 as:

        E,Γ |- A:s      E,Γ::(a:A) |- B:s'
        ----------------------------------
            E,Γ ⊦ ∀a:A,B:s''

One of the trivial cases whose description was left out from the book is
this:
s = Prop
s' = s'' = Set

        E,Γ |- A:Prop      E,Γ::(a:A) |- B:Set
        ----------------------------------
            E,Γ |- ∀a:A,B:Set

or perhaps the special case were
`a' does not occur free in `B':

        E,Γ |- A:Prop      E,Γ |- B:Set
        ----------------------------------
            E,Γ |- A->B:Set

Is it possible to give some meaningful examples of terms that can be
constructed this way?

Thanks in advance for advice.