From Tuto0 Require Import Loader.

HelloWorld.

Lemma test : True.
Proof.
hello_world.
Abort.