Goal:
  
  A : Type
  P : list A → list A → A → A → Type
  L2 : list A
  H : 0 = #|L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < 0
        → nth_error [] n = Some x1
          → nth_error L2 n = Some x2 → P [] (skipn (S n) L2) x1 x2
  ============================
   (All2_fold P [] L2)


DEBUG:Going to execute:
destruct L2

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  H : 0 = #|[]|
  X : ∀ (n : nat) (x1 x2 : A),
        n < 0
        → nth_error [] n = Some x1
          → nth_error [] n = Some x2 → P [] (skipn (S n) []) x1 x2
  ============================
   (All2_fold P [] [])

  
  A : Type
  P : list A → list A → A → A → Type
  a : A
  L2 : list A
  H : 0 = #|a :: L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < 0
        → nth_error [] n = Some x1
          → nth_error (a :: L2) n = Some x2
            → P [] (skipn (S n) (a :: L2)) x1 x2
  ============================
   (All2_fold P [] (a :: L2))


DEBUG:Going to execute:
inv H
DEBUG LTAC Evaluated term: L2

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  H : 0 = #|[]|
  X : ∀ (n : nat) (x1 x2 : A),
        n < 0
        → nth_error [] n = Some x1
          → nth_error [] n = Some x2 → P [] (skipn (S n) []) x1 x2
  ============================
   (All2_fold P [] [])

  
  A : Type
  P : list A → list A → A → A → Type
  a : A
  L2 : list A
  H : 0 = #|a :: L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < 0
        → nth_error [] n = Some x1
          → nth_error (a :: L2) n = Some x2
            → P [] (skipn (S n) (a :: L2)) x1 x2
  ============================
   (All2_fold P [] (a :: L2))


DEBUG:Going to execute:
fun H => inversion_clear H