Goal:
    A : Type  f : nat → A  m : nat  n : nat
  ============================
   (n < m ↔ nth_error (unfold m f) n = Some (f n))


DEBUG:Going to execute:
induction m in n |- *

Goals:
    A : Type  f : nat → A  n : nat
  ============================
   (n < 0 ↔ nth_error (unfold 0 f) n = Some (f n))

  
  A : Type
  f : nat → A
  m : nat
  n : nat
  IHm : ∀ n : nat, n < m ↔ nth_error (unfold m f) n = Some (f n)
  ============================
   (n < S m ↔ nth_error (unfold (S m) f) n = Some (f n))


DEBUG:Going to execute:
split
DEBUG LTAC Evaluated term: m

Goals:
    A : Type  f : nat → A  n : nat
  ============================
   (n < 0 ↔ nth_error (unfold 0 f) n = Some (f n))

  
  A : Type
  f : nat → A
  m : nat
  n : nat
  IHm : ∀ n : nat, n < m ↔ nth_error (unfold m f) n = Some (f n)
  ============================
   (n < S m ↔ nth_error (unfold (S m) f) n = Some (f n))


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::split@0>

Goals:
    A : Type  f : nat → A  n : nat
  ============================
   (n < 0 → nth_error (unfold 0 f) n = Some (f n))

    A : Type  f : nat → A  n : nat
  ============================
   (nth_error (unfold 0 f) n = Some (f n) → n < 0)

  
  A : Type
  f : nat → A
  m : nat
  n : nat
  IHm : ∀ n : nat, n < m ↔ nth_error (unfold m f) n = Some (f n)
  ============================
   (n < S m → nth_error (unfold (S m) f) n = Some (f n))

  
  A : Type
  f : nat → A
  m : nat
  n : nat
  IHm : ∀ n : nat, n < m ↔ nth_error (unfold m f) n = Some (f n)
  ============================
   (nth_error (unfold (S m) f) n = Some (f n) → n < S m)


DEBUG:Going to execute:
intros Hn

Goals:
    A : Type  f : nat → A  n : nat  Hn : n < 0
  ============================
   (nth_error (unfold 0 f) n = Some (f n))

  
  A : Type
  f : nat → A
  n : nat
  Hn : nth_error (unfold 0 f) n = Some (f n)
  ============================
   (n < 0)

  
  A : Type
  f : nat → A
  m : nat
  n : nat
  IHm : ∀ n : nat, n < m ↔ nth_error (unfold m f) n = Some (f n)
  Hn : n < S m
  ============================
   (nth_error (unfold (S m) f) n = Some (f n))

  
  A : Type
  f : nat → A
  m : nat
  n : nat
  IHm : ∀ n : nat, n < m ↔ nth_error (unfold m f) n = Some (f n)
  Hn : nth_error (unfold (S m) f) n = Some (f n)
  ============================
   (n < S m)


DEBUG:Going to execute:
try lia