Finite.v

(* equality on boolean predicates on a finite type is decidable *)
  Lemma pred_eq_dec_aux {A: Type} (l: list A) :
    forall (p1 p2: A -> bool), {forall a, In a l -> p1 a = p2 a} + {~(forall a, In a l -> p1 a = p2 a)}.
  Proof.
    induction l as [| x xs IHxs].
    (* nil case *)
    intros p1 p2. left.
    intros a Hin. inversion Hin.
    (* list of the form x:xs *)
    intros p1 p2.
    (* case distinction on whether p1 x = p2 x *)
    Require Import Coq.Bool.Bool.
    destruct (bool_dec (p1 x) (p2 x)) as [H12eqx | H12neqx].
    (* case p1 x = p2 x *)
    (* case distinction on whether p1 and p2 agree on xs *)
    destruct (IHxs p1 p2) as [H12eqxs | H12neqxs].
    (* case where p1 and p2 agree on xs *)
    left. intros a Hin.
    apply in_inv in Hin. destruct Hin as [Hx | Hxs].
    rewrite -> Hx in H12eqx. assumption.
    apply H12eqxs. assumption.
    (* p1 x = p2 x but p1 and p2 don't agree on xs *)
    right.
    intro H. apply H12neqxs. intro a. specialize (H a). intro  Hin. apply H. simpl.   right. assumption.
    (* case where p1 x <> p2 x *)
    right.
    intro H. apply H12neqx. specialize (H x). apply H. simpl. left. trivial.
  Qed.

  Lemma pred_eq_dec {A: Type} (l: list A) :
    (forall a: A, In a l) ->
    forall (p1 p2: A -> bool), {forall a, p1 a = p2 a} + {~(forall a,  p1 a = p2 a)}.
  Proof.
    intros Hcov p1 p2.
    destruct (pred_eq_dec_aux l p1 p2) as [Heq | Hneq].
    (* case where p1 and p2 are equal *)
    left.
    intro a. apply Heq. apply (Hcov a).
    (* case where p1 and p2 are different *)
    right. intro H. apply Hneq. intros a Hin. apply (H a).
Qed.

Is it possible to prove 

Lemma pred_eq_dec_tmp {A: Type} (l: list A) :
  (forall a: A, In a l) ->
  forall (p1 p2: A -> bool), {p1 = p2} + {~(p1 = p2)}.
  
  without functional extentionality ?