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 =
        assume A: Set
        assume P: A→Prop
        assume Q: A→Prop
        suppose H: ex2 A λx:A.P x λx:A.Q x
          we proceed by induction on H to prove ex2 A λx:A.Q x λx:A.P x
             case ex_intro2 : x:A H0:P x H1:Q x ⇒
                the thesis becomes ex2 A λx0:A.Q x0 λx0:A.P x0
                   by (ex_intro2 . . . . H1 H0)
ex2 A λx0:A.Q x0 λx0:A.P x0
          we proved ex2 A λx:A.Q x λx:A.P x
       we proved 
          ∀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)