DEFINITION ex2_sym()
TYPE =
       ∀A:Set
         .∀P:A→Prop
           .∀Q:A→Prop.(ex2 A λx:A.P x λx:A.Q x)→(ex2 A λx:A.Q x λx:A.P x)
BODY =
Show proof