DEFINITION ex_ind()
TYPE =
       ∀A:Set.∀P:A→Prop.∀P:Prop.(∀a:A.(P a)→P)→(ex A P)→P
BODY =
Show proof