diff --git a/theories/list.v b/theories/list.v
index 78a0f2d1084d0e54071d177072adeb11f7d300e1..eb16a6bb83ba34e65d3e35894a11fc6a09c5070c 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1260,12 +1260,12 @@ Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2,
   | _, [] => right (prefix_of_nil_not _ _)
   | x :: l1, y :: l2 =>
     match decide_rel (=) x y with
-    | left Exy =>
+    | left Hxy =>
       match go l1 l2 with
-      | left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Exy Hl1l2)
+      | left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Hxy Hl1l2)
       | right Hl1l2 => right (Hl1l2 ∘ prefix_of_cons_inv_2 _ _ _ _)
       end
-    | right Exy => right (Exy ∘ prefix_of_cons_inv_1 _ _ _ _)
+    | right Hxy => right (Hxy ∘ prefix_of_cons_inv_1 _ _ _ _)
     end
   end.
 
diff --git a/theories/numbers.v b/theories/numbers.v
index 84a7ce61ccf53e0051be84258193a4cf4d278752..264f7ee346c8a61a82f92a71c25b4690a42d8de6 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -500,11 +500,6 @@ Qed.
 Lemma Z_to_option_of_nat x : Z_to_option_nat (Z.of_nat x) = Some x.
 Proof. apply Z_to_option_nat_Some_alt. auto using Nat2Z.is_nonneg. Qed.
 
-(** The function [Z_of_sumbool] converts a sumbool [P] into an integer
-by yielding one if [P] and zero if [Q]. *)
-Definition Z_of_sumbool {P Q : Prop} (p : {P} + {Q} ) : Z :=
-  (if p then 1 else 0)%Z.
-
 (** Some correspondence lemmas between [nat] and [N] that are not part of the
 standard library. We declare a hint database [natify] to rewrite a goal
 involving [N] into a corresponding variant involving [nat]. *)
diff --git a/theories/option.v b/theories/option.v
index 626418319867c2bda0c2b5aa91886f90ef8077ad..5d4a9170d44e74614bd71df488160dc885dea94e 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -209,14 +209,16 @@ Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
     match x with Some _ => idtac | None => idtac | _ => fail 1 end;
     let y := fresh in destruct o as [y|] eqn:?;
       [change (x = f y) in H|change (x = None) in H]
-  | H : fmap (M:=option) _ ?o = ?x |- _ =>
+  | H : fmap (M:=option) ?f ?o = ?x |- _ =>
     match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match x with Some _ => idtac | None => idtac | _ => fail 1 end;
-    destruct o eqn:?
-  | H : ?x = fmap (M:=option) _ ?o |- _ =>
+    let y := fresh in destruct o as [y|] eqn:?;
+      [change (Some (f y) = x) in H|change (None = x) in H]
+  | H : ?x = fmap (M:=option) ?f ?o |- _ =>
     match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match x with Some _ => idtac | None => idtac | _ => fail 1 end;
-    destruct o eqn:?
+    let y := fresh in destruct o as [y|] eqn:?;
+      [change (x = Some (f y)) in H|change (x = None) in H]
   | _ => progress case_decide
   | _ => progress case_option_guard
   end.