\forall (A: Type[0]).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to
Prop))).((ex2 A (\lambda (x: A).(P x)) (\lambda (x: A).(Q x))) \to (ex2 A
(\lambda (x: A).(Q x)) (\lambda (x: A).(P x))))))
\forall (A: Type[0]).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to
Prop))).((ex2 A (\lambda (x: A).(P x)) (\lambda (x: A).(Q x))) \to (ex2 A
(\lambda (x: A).(Q x)) (\lambda (x: A).(P x))))))