Can we prove the following theorem constructively, and if not, what axioms are needed?

Using Coq
1 
Lemma foo {A : Type} {B C : A -> Prop} : 
  (forall x, B x) = (forall x, C x) -> forall x : A, B x = C x.

I don’t see to see how the premise can be useful. One thought is to use propositional extensionality. Is this detour necessary?

The opposite clearly works with functional extensionality. My intuition is that this direction should work constructively, but how? Please help me out.

2

Isn’t there a stupid counter-model where Prop is interpreted as Prop × 𝔹 and forall is flagged with boolean true (and the interpretation - El - of a proposition disregards the boolean) ?

3

This statement is actually false if you assume propositional extensionality.

From Coq Require Import Utf8 Setoid PropExtensionality ssrbool ssrfun ssreflect.

Lemma not_foo : ¬ ∀ (A : Type) (B C : A → Prop), 
                    (∀ x, B x) = (∀ x, C x) → ∀ x : A, B x = C x.
Proof.
  move: (n_Sn 0) => /[swap] /(_ _ (eq 1) (eq 0)) <- //.
  apply propositional_extensionality; split => [/(_ 0) | /(_ 1)] //.
Qed.
4

ok, you guys are right. very stupid of me.

5

For what it’s worth, I don’t think it’s stupid. I thought they were equivalent too, until I looked more closely.