Definition half (x : {x : nat | even x }) : nat := let n := (proj1_sig x) in
                                                   Nat.div n 2.

Definition Nonempty {A} (l : list A) := match l with cons _ _ => True | nil => False end.


Definition notempty A (l: list A) : Prop := forall (P : list A -> Prop),
                                              (forall (y : list A), forall (c: A) ,P(cons y c)) -> P l.

Definition mylist := (cons (cons (cons nil 3) 2) 1).

Theorem mylistnotempty : notempty nat (mylist).
Proof.
  unfold notempty.
  intro.
  intro.
  apply H.
Qed.

Definition back (A : Set) (nel : {x: (list A) | (notempty A x) })  : list A := let l := proj1_sig nel in
                                                                               match l with
                                                                                 | cons tail head => tail
                                                                                 | nil => match (proj2_sig nel) Nonempty (fun _ _ => I) with end
                                                                               end.