DEFINITION ex2_ind()
TYPE =
       ∀A:Set
         .∀P:A→Prop
           .∀Q:A→Prop
             .∀P:Prop.(∀a:A.(P a)→(Q a)→P)→(ex2 A P Q)→P
BODY =
Show proof