λ(_ : A) → λ(_ : B) → _@1