diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index c54e70b0d8a4715d93db217fff62fedc1f2e2e35..49aad330074589d0370cfb6282fa7c6bf28a14e6 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -288,10 +288,6 @@ End freshness.
 
 (* Deallocation is not a local update. The trouble is that if we own {[ i ↦ x ]},
    then the frame could always own "unit x", and prevent deallocation. *)
-(*
-Lemma option_fmap_op {B : cmraT} (f : A → B) (mx my : option A) : f <$> mx ⋅ my = (f <$> mx) ⋅ (f <$> my).
-Proof. destruct mx, my; simpl; try done.
-*)
 Global Instance map_alter_update `{!LocalUpdate P f} i :
   LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ P x) (alter f i).
 Proof.