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...