使用命题函数的函数外延性证明cup交换律的问题

我将类型X的对象集合表示为函数X -> Prop，并定义了并集操作cup：

Definition cup {X : Type} (a b : X -> Prop) : X -> Prop := fun (x : X) => a x \/ b x.

在证明基础性质时，我尝试用普通等式形式的函数外延性公理证明cup的交换律，但遇到了Setoid重写错误。最小复现代码及错误信息如下：

Require Import Setoid.

Axiom func_eq : forall (X Y : Type) (f g : X -> Y), (forall (x : X), f x = g x) -> f = g.

Definition cup {X : Type} (a b : X -> Prop) : X -> Prop := fun (x : X) => a x \/ b x.

Theorem cup_comm : forall (X : Type) (a b : X -> Prop), cup a b = cup b a.
Proof.
    intros. apply func_eq. intros. unfold cup.
    rewrite or_comm. (* <-------- ERROR HERE *)

错误信息：

setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?X17==[X a b x |- relation Prop] (internal placeholder) {?r}
 ?X18==[X a b x (do_subrelation:=Morphisms.do_subrelation) |-
         Morphisms.Proper (iff ==> ?r ==> Basics.flip Basics.impl) eq]
         (internal placeholder) {?p}
 ?X19==[X a b x |- Morphisms.ProperProxy ?r (b x \/ a x)]
         (internal placeholder) {?p0}
TYPECLASSES:?X17 ?X18 ?X19
SHELF:||
FUTURE GOALS STACK:?X19 ?X18 ?X17||

我尝试简化证明状态但无法解决，甚至在证明forall (P Q : Prop), (P <-> Q) -> P = Q时也遇到类似问题。不过改用双条件（<->）形式的函数外延性公理后，成功完成了证明：

Require Import Setoid.

Axiom func_eq_iff : forall (X : Type) (f g : X -> Prop), (forall (x : X), f x <-> g x) -> f = g.

Definition cup {X : Type} (a b : X -> Prop) : X -> Prop := fun (x : X) => a x \/ b x.

Theorem cup_comm : forall (X : Type) (a b : X -> Prop), cup a b = cup b a.
Proof.
    intros. unfold cup. apply func_eq_iff. intros. rewrite or_comm. reflexivity.
Qed.

已知(P <-> Q) <-> (P = Q)公理逻辑一致，且可推导出上述双条件形式的函数外延性。我想咨询两个问题：

• 是否只能使用此类双条件形式的公理来证明该定理？
• 为何之前用普通函数外延性公理时，Setoid重写会失败？

内容的提问来源于stack exchange，提问作者Cruz Jean