The Boogaloo type checker cannot infer types.
In practice it means that every function application,
where the the function return type is generic and does not occur among the arguments,
-has to be surrounded by a coercion.
+has to be surrounded by a coercion.
Except for definition axioms mentioned above, all other axioms are ignored.