diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 0b473a7925775b4b536967dedbb2d3fe349609b8..010d4afe218775ec768a24b23e288f5db7fd1ca7 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -21,7 +21,7 @@ Notation map := (cFunctor_map F).
 Fixpoint A (k : nat) : ofeT :=
   match k with 0 => unitC | S k => F (A k) end.
 Local Instance: ∀ k, Cofe (A k).
-Proof using Fcofe. induction 0; apply _. Defined.
+Proof using Fcofe. induction k; apply _. Defined.
 Fixpoint f (k : nat) : A k -n> A (S k) :=
   match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
 with g (k : nat) : A (S k) -n> A k :=
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 4843e6f031d09868a0d62ff459881617f1d9b760..50c494b91b82c4c8b2dbbc7d8539d9c531d7a30f 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -64,7 +64,7 @@ Qed.
 Global Instance frame_step_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step.
 Proof. move=> ?? /collection_equiv_spec [??]; split; by apply frame_step_mono. Qed.
 Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed.
-Proof. destruct 3; constructor; intros until 0; setoid_subst; eauto. Qed.
+Proof. destruct 3; constructor; intros; setoid_subst; eauto. Qed.
 Global Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed.
 Proof. by split; apply closed_proper'. Qed.
 Global Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up.