Definition of ex2 on 4.2.1

[gaxiiiiiiiiiiii]

The book saids:

Inductive ex2 A P Q : Prop := ex_intro2 x of P x & Q x.

I guess it should be like this:

Inductive ex2 A P Q : Prop := ex_intro2 (x : A) of P x & Q x.