An exact proof term for the current goal is (λA B ⇒ andEL (A → B) (B → A)).