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