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