как использовать модули, чтобы скрыть леммы в coq?

У меня есть теорема T, ее доказательство и бесчисленное количество лемм, использованных при ее доказательстве.

Я хотел бы скрыть леммы и сделать доступной только теорему - главным образом потому, что я не хочу думать о хороших, глобальных именах для лемм.

Могу ли я поместить теорему, ее доказательство и леммы в модуль, ограниченный типом модуля, и сделать доступной только теорему?

Что-то типа:

Module Type T_MY_T.
End T_MY_T.

Module T_My_theorem : T_MY_T.
  Lemma L1: ...
  Proof. Admitted.
  Lemma L2: ...
  Proof. Admitted.
  Theorem My_Great_Theorem: ...
  Proof. apply L1; apply L2. Qed.
End T_My_theorem.

Если да, может ли кто-нибудь опубликовать или указать мне простой пример?