Goal:
  
  ============================
   (nth_error ?list_all 0 = Some I)


DEBUG:Going to execute:
unshelve
(repeat
  match goal with
  | |- nth_error (?x :: _) 0 = ?rhs => change (Some x = rhs)
  | |- nth_error (_ :: ?xs) (S ?n) = ?rhs => change (nth_error xs n = rhs)
  | |- nth_error ?ev _ = ?rhs =>
        is_evar ev; (let __ := open_constr:((eq_refl : ev = _ :: _)) in
                     idtac)
  | |- Some _ = Some _ => reflexivity
  end)
Level 0: Backtrace:

No product even after head-reduction.
Level 0: Backtrace:

No product even after head-reduction.
Level 0: Backtrace:

No product even after head-reduction.
Level 1: Backtrace:

No product even after head-reduction.
Level 0: Backtrace:

No product even after head-reduction.