Nonempty list safe head

nelist.v

Require Import List.
Import ListNotations.

Section nelist. 
  Variable (A : Type).

Definition nelist : Type := {l : list A | l <> nil}.

Definition safe_head (l : nelist) : A. 
  refine (match proj1_sig l as y' return y' <> [] -> _ with
            | [] => fun H => _
            | x :: l' => fun _ => x
          end _).
  - congruence.
  - exact (proj2_sig l).
Defined.
End nelist.