Coq中无法在存在量词下重写等价定理的问题求助

我的当前情况 #

我已经自行证明了这个等价定理：

Theorem and_distributes_over_or : forall P Q R : Prop, P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).

现在我的证明目标如下：

exists x0 : A, f x0 = y /\ (x = x0 \/ In x0 xs)

注：正在学习《Logical Foundations》构造逻辑章节的In_map_iff练习，请不要直接给出练习答案！

尝试操作与报错情况 #

我想把目标里的合取分配到析取上，于是使用了rewrite and_distributes_over_or命令，期望得到的目标是：

exists x0 : A, (f x0 = y /\ x = x0) \/ (f x0 = y /\ In x0 xs)

但Coq直接抛出了错误：

Found no subterm matching "?P /\ (?P0 \/ ?P1)" in the current goal.

疑问与求助点 #

明明我能直观看到目标里f x0 = y /\ (x = x0 \/ In x0 xs)这部分完全符合定理的左式结构，为什么Coq识别不到存在量词下面的这个子项呢？有没有可行的解决办法能实现我想要的重写效果？

之前我也看过类似问题，但那篇内容是针对假设中的重写场景，和我当前的情况不匹配。

内容的提问来源于stack exchange，提问作者Benjamin Hodgson