I have a question that I can't solve:
Given the simply typed lambda-calculus with call-by-value evaluation and the regular inference rules for abstraction, application and variables. If I just add the Unit type with the constant *:Unit, is the following true?
If t -> t' and t':T, then t:T
I suspect the answer is no, but I can't come up with a counterexample.