The desired signature of if_then_else_fi is forall t . bool -> t -> t -> t. Unfortunately, the K frontend does not support that, so it has the more generic signature bool -> klist -> klist -> klist. This would result in if_then_else_fi being always injected.