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


DEBUG:Going to execute:
congruence