diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index 5ffa5d53186127eadbf121878ac50257b2d80c48..530ccf48152800eff52501c3d77d4e2917a00831 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -171,7 +171,7 @@ Proof.
     by iApply "HΦ".
 Qed.
 
-Lemma prog_fun_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
+Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
   wp_apply (start_chan_proto_spec prot_loop); iIntros (c) "Hc".