The K combinator is used to trigger lambda conversions. Due to user demand, it is turned off by default.
K_conversion [T1:TYPE, T2:TYPE] : THEORY BEGIN
K conversion((x:T1))((y:T2)): T1 = x; END K_conversion