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


DEBUG:Going to execute:
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