Are we forced to check?

[HuStmpHrrr]

It appears to me that we can always infer a type. I suppose the final type is not necessary if it's not given? the inference algorithm should always infer the most precise type. Do we have a theorem stating this?

[HuStmpHrrr]

I think that theorem is a variant of
https://github.com/Beluga-lang/McLTT/blob/922419255d4e95251c32c234f274c06d7160f58c/theories/Algorithmic/Typing/Lemmas.v#L280-L283

[Ailrun]

We don't need to. I provided it there just as a testing convenience, but one can simulate that with (fun (x : A) -> x) e instead of e : A (or even with the "let binding" @Antoine-something is implementing)