redlizard.v

Require Import List.
Import ListNotations.

Section redlizard.
  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}.
    refine match l with
    | [] => fun H => False_rect _ _
    | x :: l' => fun H => if P_dec x then exist _ x _ else getP' l' _
    end.
    - firstorder.
    - auto.
    - simpl in *. firstorder. subst. congruence.
  Defined.

  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 redlizard.