Goal:
  
  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
  a0 : A
  L2 : list A
  H : S #|L1| = #|a0 :: L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < S #|L1|
        → nth_error (a :: L1) n = Some x1
          → nth_error (a0 :: L2) n = Some x2
            → P (skipn n L1) (skipn (S n) (a0 :: L2)) x1 x2
  H1 : #|L1| = #|L2|
  ============================
   (P L1 L2 a a0)


DEBUG:Going to execute:
eapply (X 0)

Goals:
  
  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
  a0 : A
  L2 : list A
  H : S #|L1| = #|a0 :: L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < S #|L1|
        → nth_error (a :: L1) n = Some x1
          → nth_error (a0 :: L2) n = Some x2
            → P (skipn n L1) (skipn (S n) (a0 :: L2)) x1 x2
  H1 : #|L1| = #|L2|
  ============================
   (0 < S #|L1|)

  
  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
  a0 : A
  L2 : list A
  H : S #|L1| = #|a0 :: L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < S #|L1|
        → nth_error (a :: L1) n = Some x1
          → nth_error (a0 :: L2) n = Some x2
            → P (skipn n L1) (skipn (S n) (a0 :: L2)) x1 x2
  H1 : #|L1| = #|L2|
  ============================
   (nth_error (a :: L1) 0 = Some a)

  
  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
  a0 : A
  L2 : list A
  H : S #|L1| = #|a0 :: L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < S #|L1|
        → nth_error (a :: L1) n = Some x1
          → nth_error (a0 :: L2) n = Some x2
            → P (skipn n L1) (skipn (S n) (a0 :: L2)) x1 x2
  H1 : #|L1| = #|L2|
  ============================
   (nth_error (a0 :: L2) 0 = Some a0)


DEBUG:Going to execute:
cbn
DEBUG LTAC Evaluated term: (X 0)

Goals:
  
  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
  a0 : A
  L2 : list A
  H : S #|L1| = #|a0 :: L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < S #|L1|
        → nth_error (a :: L1) n = Some x1
          → nth_error (a0 :: L2) n = Some x2
            → P (skipn n L1) (skipn (S n) (a0 :: L2)) x1 x2
  H1 : #|L1| = #|L2|
  ============================
   (0 < S #|L1|)

  
  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
  a0 : A
  L2 : list A
  H : S #|L1| = #|a0 :: L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < S #|L1|
        → nth_error (a :: L1) n = Some x1
          → nth_error (a0 :: L2) n = Some x2
            → P (skipn n L1) (skipn (S n) (a0 :: L2)) x1 x2
  H1 : #|L1| = #|L2|
  ============================
   (Some a = Some a)

  
  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
  a0 : A
  L2 : list A
  H : S #|L1| = #|a0 :: L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < S #|L1|
        → nth_error (a :: L1) n = Some x1
          → nth_error (a0 :: L2) n = Some x2
            → P (skipn n L1) (skipn (S n) (a0 :: L2)) x1 x2
  H1 : #|L1| = #|L2|
  ============================
   (Some a0 = Some a0)


DEBUG:Going to execute:
eauto

Goals:
  
  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
  a0 : A
  L2 : list A
  H : S #|L1| = #|a0 :: L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < S #|L1|
        → nth_error (a :: L1) n = Some x1
          → nth_error (a0 :: L2) n = Some x2
            → P (skipn n L1) (skipn (S n) (a0 :: L2)) x1 x2
  H1 : #|L1| = #|L2|
  ============================
   (0 < S #|L1|)

  
  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
  a0 : A
  L2 : list A
  H : S #|L1| = #|a0 :: L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < S #|L1|
        → nth_error (a :: L1) n = Some x1
          → nth_error (a0 :: L2) n = Some x2
            → P (skipn n L1) (skipn (S n) (a0 :: L2)) x1 x2
  H1 : #|L1| = #|L2|
  ============================
   (Some a = Some a)

  
  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
  a0 : A
  L2 : list A
  H : S #|L1| = #|a0 :: L2|
  X : ∀ (n : nat) (x1 x2 : A),
        n < S #|L1|
        → nth_error (a :: L1) n = Some x1
          → nth_error (a0 :: L2) n = Some x2
            → P (skipn n L1) (skipn (S n) (a0 :: L2)) x1 x2
  H1 : #|L1| = #|L2|
  ============================
   (Some a0 = Some a0)


DEBUG:Going to execute:
<coq-core.plugins.ltac::eauto@0> $1 $2 $3