diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index fd4dc0e9352a87ccd6e05b4bddefd0063df37c24..69a018f5c095634b77e232a7761e6fb617c187f9 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -91,7 +91,7 @@ Section heap.
     rewrite to_heap_insert big_sepM_insert //.
     rewrite (map_insert_singleton_op (to_heap σ));
       last rewrite lookup_fmap Hl; auto.
-    by rewrite auto_own_op IH.
+    by rewrite auth_own_op IH.
   Qed.
 
   Context `{heapG Σ}.
@@ -103,7 +103,7 @@ Section heap.
   (** General properties of mapsto *)
   Lemma heap_mapsto_disjoint l v1 v2 : (l ↦ v1 ★ l ↦ v2)%I ⊑ False.
   Proof.
-    rewrite heap_mapsto_eq -auto_own_op auto_own_valid map_op_singleton.
+    rewrite heap_mapsto_eq -auth_own_op auth_own_valid map_op_singleton.
     rewrite map_validI (forall_elim l) lookup_singleton.
     by rewrite option_validI excl_validI.
   Qed.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 9e4634b932ce8c7494a14e9dd06a06585e511cf0..c08eb41867ed2c5f21d3c9d0caab8e7d4d8257be 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -40,10 +40,10 @@ Section auth.
   Proof. by rewrite /auth_own=> a b ->. Qed.
   Global Instance auth_own_proper γ : Proper ((≡) ==> (≡)) (auth_own γ).
   Proof. by rewrite /auth_own=> a b ->. Qed.
-  Lemma auto_own_op γ a b :
+  Lemma auth_own_op γ a b :
     auth_own γ (a ⋅ b) ≡ (auth_own γ a ★ auth_own γ b)%I.
   Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
-  Lemma auto_own_valid γ a : auth_own γ a ⊑ ✓ a.
+  Lemma auth_own_valid γ a : auth_own γ a ⊑ ✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
 
   Lemma auth_alloc E N a :