rrika.v

Require Import List.
Import ListNotations.

Section rrika.
  Variable A : Type.
  Variable P : A -> Prop.
  Hypothesis P_dec : forall x : A, {P x} + {~ P x}.
  

  Fixpoint getP' (l : list A) : (exists x, In x l /\ P x) -> {x : A | P x} :=
    match l with
    | [] => fun H : (exists _, In _ [] /\ _) => False_rect _ (match H with ex_intro _ a pf => proj1 pf end)
    | x :: l' => fun H => match P_dec x with 
                      | left pf => exist _ x pf 
                      | right pf => getP' l' (match H with 
                                             | ex_intro _ a wit => 
                                               ex_intro _ a (conj (match proj1 wit with
                                                                   | or_introl e => False_rect _ (pf (eq_rect_r _ (proj2 wit) e))
                                                                   | or_intror n => n
                                                                   end)
                                                                  (proj2 wit)) 
                                             end)
                      end
    end.


  Definition getP : {l : list A | (exists x, In x l /\ P x)} -> {x : A | P x} :=
    fun a => getP' (proj1_sig a) (proj2_sig a).
End rrika.