diff --git a/algebra/agree.v b/algebra/agree.v
index 7b8641655090fe0ed4fa5572b3ef863d2791b893..a71d7a4d218576cbf7067f507fc73d52badf2e3f 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -61,7 +61,7 @@ Instance agree_unit : Unit (agree A) := id.
 Instance agree_minus : Minus (agree A) := λ x y, x.
 Instance: Comm (≡) (@op (agree A) _).
 Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
-Definition agree_idemp (x : agree A) : x ⋅ x ≡ x.
+Lemma agree_idemp (x : agree A) : x ⋅ x ≡ x.
 Proof. split; naive_solver. Qed.
 Instance: ∀ n : nat, Proper (dist n ==> impl) (@validN (agree A) _ n).
 Proof.
diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 9683f606f41147a6e0038a8e63cd39fe76955706..3adbb7eef693fa8d43e231baf5b3cfe06ff1dab3 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -47,3 +47,5 @@ Proof.
 Qed.
 
 Canonical Structure dec_agreeRA : cmraT := discreteRA dec_agree_ra.
+
+End dec_agree.
\ No newline at end of file