Declare ML Module "good_plugin".

magic.

Lemma x : True. Proof. trivial. Qed.