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


DEBUG:Going to execute:
apply All2_from_nth_error

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

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


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

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

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


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