k :: Nat -> Nat -> Nat := \x.\y.x;