Goal:
  
  A : Type
  B : Type
  f : A → B
  H : ∀ l : list A, nth_error (map f l) 0 = option_map f (nth_error l 0)
  l : list A
  ============================
   (nth_error (map f l) 1 = option_map f (nth_error l 1))


DEBUG:Going to execute:
case not_locked_false_eq_true; Ltac.assumption
Level 1: Backtrace:

In environment
A : Type
B : Type
f : A → B
H : ∀ l : list A, nth_error (map f l) 0 = option_map f (nth_error l 0)
l : list A
Unable to unify "option_map f (nth_error l 1)" with 
"nth_error (map f l) 1".
Level 0: Backtrace:

In environment
A : Type
B : Type
f : A → B
H : ∀ l : list A, nth_error (map f l) 0 = option_map f (nth_error l 0)
l : list A
Unable to unify "option_map f (nth_error l 1)" with 
"nth_error (map f l) 1".
Level 0: Backtrace:

No applicable tactic.
Level 0: Backtrace:

No applicable tactic.