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


DEBUG:Going to execute:
induction L1

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

  
  A : Type
  a : A
  L1 : list A
  P : list A → list A → A → A → Type
  IHL1 : ∀ L2 : list A,
           #|L1| = #|L2|
           → (∀ (n : nat) (x1 x2 : A),
                n < #|L1|
                → nth_error L1 n = Some x1
                  → nth_error L2 n = Some x2
                    → P (skipn (S n) L1) (skipn (S n) L2) x1 x2)
             → All2_fold P L1 L2
  ============================
   (∀ L2 : list A,
      #|a :: L1| = #|L2|
      → (∀ (n : nat) (x1 x2 : A),
           n < #|a :: L1|
           → nth_error (a :: L1) n = Some x1
             → nth_error L2 n = Some x2
               → P (skipn (S n) (a :: L1)) (skipn (S n) L2) x1 x2)
        → All2_fold P (a :: L1) L2)


DEBUG:Going to execute:
cbn
DEBUG LTAC Evaluated term: L1

Goals:
    A : Type  P : list A → list A → A → A → Type
  ============================
   (∀ L2 : list A,
      0 = #|L2|
      → (∀ (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)

  
  A : Type
  a : A
  L1 : list A
  P : list A → list A → A → A → Type
  IHL1 : ∀ L2 : list A,
           #|L1| = #|L2|
           → (∀ (n : nat) (x1 x2 : A),
                n < #|L1|
                → nth_error L1 n = Some x1
                  → nth_error L2 n = Some x2
                    → P (skipn (S n) L1) (skipn (S n) L2) x1 x2)
             → All2_fold P L1 L2
  ============================
   (∀ L2 : list A,
      S #|L1| = #|L2|
      → (∀ (n : nat) (x1 x2 : A),
           n < S #|L1|
           → nth_error (a :: L1) n = Some x1
             → nth_error L2 n = Some x2
               → P (skipn n L1) (skipn (S n) L2) x1 x2)
        → All2_fold P (a :: L1) L2)


DEBUG:Going to execute:
intros