First attempt at predicated lists in Coq

predicated_list.v

Require Import Coq.Arith.Arith.

Section predicated_list.
  Variable A : Type.
  Variable bin_rel : A -> A -> Prop.

  Hypothesis bin_rel_trans : forall a b c : A, bin_rel c b -> bin_rel b a -> bin_rel c a.

  Set Implicit Arguments.

  Inductive predicated_list : (A -> Prop) -> Type :=
  | predicated_nil  : predicated_list (fun x : A => True)
  | predicated_cons : forall (p : A -> Prop) (x : A),
                        p x -> predicated_list p -> predicated_list (bin_rel x).

  Fixpoint element_in
           (p : A -> Prop)
           (x : A)
           (l : predicated_list p) : Prop :=
    match l with
      | predicated_nil => False
      | predicated_cons _ y _ rest => x = y \/ element_in x rest
    end.

  Unset Implicit Arguments.

  Definition starts_with (p : A -> Prop) (l : predicated_list p) (x : A) :=
    match l with
      | predicated_nil => False
      | predicated_cons _ y _ _ => x = y
    end.

  Fixpoint bin_rel_rest (p : A -> Prop) (l : predicated_list p) :
    forall x y : A, p x -> element_in y l -> bin_rel y x.
  Proof.
    (* if l is empty, element_in _  y l is False => contradiction *)
    case l.
    contradiction.

    unfold element_in.
    intros.
    decompose [or] H0.

    (* if l starts with y, p is the proof we're looking for *)
    replace y with x.
    assumption.

    apply (bin_rel_trans x0 x y).
    apply (bin_rel_rest p0 p2 x y p1 H1).
    assumption.
  Defined.
End predicated_list.