diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 515028163eaa79d7aa529cfeb42c6c6b8e0ffe08..9c5c79f6339d829d72f60dfe17df2451de72d6a2 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -109,14 +109,14 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
 Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
   gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
 Proof.
-  assert (i = i2 + i1) by lia; simplify_eq/=. revert j x H1.
+  assert (i = i2 + i1) by lia; move:H1=>H1; simplify_eq/=. revert j x H1.
   induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=;
     [by rewrite coerce_id|by rewrite g_coerce IH].
 Qed.
 Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) :
   coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
 Proof.
-  assert (i = i1 + i2) by lia; simplify_eq/=.
+  assert (i = i1 + i2) by lia; move:H1=>H1; simplify_eq/=.
   induction i1 as [|i1 IH]; simplify_eq/=;
     [by rewrite coerce_id|by rewrite coerce_f IH].
 Qed.
diff --git a/prelude/collections.v b/prelude/collections.v
index 850226e1571c4a65910ed62910d035490568c18c..ef7383d529cf25477858fe854a4fb7bbf46bfc2f 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -390,7 +390,7 @@ Section simple_collection.
     split.
     - induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
       setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver.
-    - intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
+    - intros [X [Hx]]. induction Hx; simpl; [by apply elem_of_union_l |].
       intros. apply elem_of_union_r; auto.
   Qed.
 
diff --git a/prelude/list.v b/prelude/list.v
index 59b26331813bf82dc7cd243e88f8721e7b9fd82e..9a384897ea4fdf4aa708d14ac60121cd48fbd247 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -926,7 +926,7 @@ Proof. by destruct n. Qed.
 Lemma drop_length l n : length (drop n l) = length l - n.
 Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
 Lemma drop_ge l n : length l ≤ n → drop n l = [].
-Proof. revert n. induction l; intros [|??]; simpl in *; auto with lia. Qed.
+Proof. revert n. induction l; intros [|?]; simpl in *; auto with lia. Qed.
 Lemma drop_all l : drop (length l) l = [].
 Proof. by apply drop_ge. Qed.
 Lemma drop_drop l n1 n2 : drop n1 (drop n2 l) = drop (n2 + n1) l.
@@ -2828,7 +2828,7 @@ Section fmap.
     (∀ x, f x = y) → f <$> l = replicate (length l) y.
   Proof. intros; induction l; f_equal/=; auto. Qed.
   Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
-  Proof. revert i. induction l; by intros [|]. Qed.
+  Proof. revert i. induction l; intros [|n]; by try revert n. Qed.
   Lemma list_lookup_fmap_inv l i x :
     (f <$> l) !! i = Some x → ∃ y, x = f y ∧ l !! i = Some y.
   Proof.