diff --git a/theories/examples/encoding_proofs.v b/theories/examples/proofs_enc.v
similarity index 98%
rename from theories/examples/encoding_proofs.v
rename to theories/examples/proofs_enc.v
index 16850a5d0e152687191edef7f5b2530f4fa799fa..b0eb0d9f2ccad09a1170d48c86474915bd0442ef 100644
--- a/theories/examples/encoding_proofs.v
+++ b/theories/examples/proofs_enc.v
@@ -6,7 +6,7 @@ From iris.base_logic Require Import invariants.
 From osiris.encodings Require Import stype_enc.
 From osiris.examples Require Import examples.
 
-Section ExampleProofsEncodings.
+Section ExampleProofsEnc.
   Context `{!heapG Σ} {N : namespace}.
   Context `{!logrelG val Σ}.
 
@@ -115,4 +115,4 @@ Section ExampleProofsEncodings.
       by iApply "HΦ".
   Qed.
 
-End ExampleProofsEncodings.
\ No newline at end of file
+End ExampleProofsEnc.
\ No newline at end of file