Goal:
    A : Type  l : list A
  ============================
   (∀ n : nat, (∑ x : A, nth_error l n = Some x) <~> n < #|l|)


DEBUG:Going to execute:
induction l

Goals:
    A : Type
  ============================
   (∀ n : nat, (∑ x : A, nth_error [] n = Some x) <~> n < #|[]|)

  
  A : Type
  a : A
  l : list A
  IHl : ∀ n : nat, (∑ x : A, nth_error l n = Some x) <~> n < #|l|
  ============================
   (∀ n : nat, (∑ x : A, nth_error (a :: l) n = Some x) <~> n < #|a :: l|)


DEBUG:Going to execute:
destruct n
DEBUG LTAC Evaluated term: l

Goals:
    A : Type
  ============================
   ((∑ x : A, nth_error [] 0 = Some x) <~> 0 < #|[]|)

    A : Type  n : nat
  ============================
   ((∑ x : A, nth_error [] (S n) = Some x) <~> S n < #|[]|)

  
  A : Type
  a : A
  l : list A
  IHl : ∀ n : nat, (∑ x : A, nth_error l n = Some x) <~> n < #|l|
  ============================
   ((∑ x : A, nth_error (a :: l) 0 = Some x) <~> 0 < #|a :: l|)

  
  A : Type
  a : A
  l : list A
  IHl : ∀ n : nat, (∑ x : A, nth_error l n = Some x) <~> n < #|l|
  n : nat
  ============================
   ((∑ x : A, nth_error (a :: l) (S n) = Some x) <~> S n < #|a :: l|)


DEBUG:Going to execute:
simpl