Goal:
  
  A : Type
  B : Type
  P : list A → list A → A → A → B → Type
  ls2 : list A
  ls3 : list A
  H : [] ≠ [] ∨ #|ls2| = #|ls3|
  H0 : #|ls2| = #|ls3|
  ============================
   (All2_fold (λ (l1 l2 : list A) (x y : A), All (P l1 l2 x y) []) ls2 ls3)


DEBUG:Going to execute:
apply All2_fold_from_nth_error

Goals:
  
  A : Type
  B : Type
  P : list A → list A → A → A → B → Type
  ls2 : list A
  ls3 : list A
  H : [] ≠ [] ∨ #|ls2| = #|ls3|
  H0 : #|ls2| = #|ls3|
  ============================
   (#|ls2| = #|ls3|)

  
  A : Type
  B : Type
  P : list A → list A → A → A → B → Type
  ls2 : list A
  ls3 : list A
  H : [] ≠ [] ∨ #|ls2| = #|ls3|
  H0 : #|ls2| = #|ls3|
  ============================
   (∀ (n : nat) (x1 x2 : A),
      n < #|ls2|
      → nth_error ls2 n = Some x1
        → nth_error ls3 n = Some x2
          → All (P (skipn (S n) ls2) (skipn (S n) ls3) x1 x2) [])


DEBUG:Going to execute:
eauto
DEBUG LTAC Evaluated term: All2_fold_from_nth_error

Goals:
  
  A : Type
  B : Type
  P : list A → list A → A → A → B → Type
  ls2 : list A
  ls3 : list A
  H : [] ≠ [] ∨ #|ls2| = #|ls3|
  H0 : #|ls2| = #|ls3|
  ============================
   (#|ls2| = #|ls3|)

  
  A : Type
  B : Type
  P : list A → list A → A → A → B → Type
  ls2 : list A
  ls3 : list A
  H : [] ≠ [] ∨ #|ls2| = #|ls3|
  H0 : #|ls2| = #|ls3|
  ============================
   (∀ (n : nat) (x1 x2 : A),
      n < #|ls2|
      → nth_error ls2 n = Some x1
        → nth_error ls3 n = Some x2
          → All (P (skipn (S n) ls2) (skipn (S n) ls3) x1 x2) [])


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