Несогласованное поведение Coq в отношении неявных параметров определений Let

Я обнаружил некоторую несогласованность поведения Coq в отношении неявных параметров.

Section foo.
  Let id1 {t : Set} (x : t) := x.
  Let id2 {t : Set} (x : t) : t. assumption. Qed.
  Check id2 (1:nat).
  Check id1 (1:nat). (* Fails with "The term "1:nat" has type "nat" while it is expected to have type "Set"." *)
End foo.

Определение Let id1 , похоже, не дает t неявно, тогда как при замене Let на Definition ошибок не возникает. Я что-то не так понял или есть это ошибка?