diff --git a/prelude/option.v b/prelude/option.v
index 865311fdcfe1bef48bf4173c765bbed27fe1c2ea..bf66ba9724d9c55d0c3c949e22c15615ee76b6af 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -306,6 +306,10 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=
| _ => rewrite decide_False by tac
| _ => rewrite option_guard_True by tac
| _ => rewrite option_guard_False by tac
+ | H : context [None ∪ _] |- _ => rewrite (left_id_L None (∪)) in H
+ | H : context [_ ∪ None] |- _ => rewrite (right_id_L None (∪)) in H
+ | |- context [None ∪ _] => rewrite (left_id_L None (∪))
+ | |- context [_ ∪ None] => rewrite (right_id_L None (∪))
end.
Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
repeat match goal with