Goal:
    A : Type  l' : list A  t : A
  ============================
   (None = Some t
    → match l' with
      | [] => None
      | x :: _ => Some x
      end = Some t)


DEBUG:Going to execute:
congruence