Goal:
  
  A : Type
  B : Type
  a : A
  L1 : list A
  P : A → B → Prop
  IHL1 : ∀ L2 : list B,
           #|L1| = #|L2|
           → (∀ (n : nat) (x1 : A) (x2 : B),
                n < #|L1|
                → nth_error L1 n = Some x1
                  → nth_error L2 n = Some x2 → P x1 x2) → 
             Forall2 P L1 L2
  b : B
  L2 : list B
  H : S #|L1| = #|b :: L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < S #|L1|
         → nth_error (a :: L1) n = Some x1
           → nth_error (b :: L2) n = Some x2 → P x1 x2
  H2 : #|L1| = #|L2|
  n : nat
  x1 : A
  x2 : B
  H1 : n < #|L1|
  H3 : nth_error L1 n = Some x1
  H4 : nth_error L2 n = Some x2
  ============================
   (P x1 x2)


DEBUG:Going to execute:
eapply (H0 (S n))

Goals:
  
  A : Type
  B : Type
  a : A
  L1 : list A
  P : A → B → Prop
  IHL1 : ∀ L2 : list B,
           #|L1| = #|L2|
           → (∀ (n : nat) (x1 : A) (x2 : B),
                n < #|L1|
                → nth_error L1 n = Some x1
                  → nth_error L2 n = Some x2 → P x1 x2) → 
             Forall2 P L1 L2
  b : B
  L2 : list B
  H : S #|L1| = #|b :: L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < S #|L1|
         → nth_error (a :: L1) n = Some x1
           → nth_error (b :: L2) n = Some x2 → P x1 x2
  H2 : #|L1| = #|L2|
  n : nat
  x1 : A
  x2 : B
  H1 : n < #|L1|
  H3 : nth_error L1 n = Some x1
  H4 : nth_error L2 n = Some x2
  ============================
   (S n < S #|L1|)

  
  A : Type
  B : Type
  a : A
  L1 : list A
  P : A → B → Prop
  IHL1 : ∀ L2 : list B,
           #|L1| = #|L2|
           → (∀ (n : nat) (x1 : A) (x2 : B),
                n < #|L1|
                → nth_error L1 n = Some x1
                  → nth_error L2 n = Some x2 → P x1 x2) → 
             Forall2 P L1 L2
  b : B
  L2 : list B
  H : S #|L1| = #|b :: L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < S #|L1|
         → nth_error (a :: L1) n = Some x1
           → nth_error (b :: L2) n = Some x2 → P x1 x2
  H2 : #|L1| = #|L2|
  n : nat
  x1 : A
  x2 : B
  H1 : n < #|L1|
  H3 : nth_error L1 n = Some x1
  H4 : nth_error L2 n = Some x2
  ============================
   (nth_error (a :: L1) (S n) = Some x1)

  
  A : Type
  B : Type
  a : A
  L1 : list A
  P : A → B → Prop
  IHL1 : ∀ L2 : list B,
           #|L1| = #|L2|
           → (∀ (n : nat) (x1 : A) (x2 : B),
                n < #|L1|
                → nth_error L1 n = Some x1
                  → nth_error L2 n = Some x2 → P x1 x2) → 
             Forall2 P L1 L2
  b : B
  L2 : list B
  H : S #|L1| = #|b :: L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < S #|L1|
         → nth_error (a :: L1) n = Some x1
           → nth_error (b :: L2) n = Some x2 → P x1 x2
  H2 : #|L1| = #|L2|
  n : nat
  x1 : A
  x2 : B
  H1 : n < #|L1|
  H3 : nth_error L1 n = Some x1
  H4 : nth_error L2 n = Some x2
  ============================
   (nth_error (b :: L2) (S n) = Some x2)


DEBUG:Going to execute:
cbn
DEBUG LTAC Evaluated term: (H0 (S n))

Goals:
  
  A : Type
  B : Type
  a : A
  L1 : list A
  P : A → B → Prop
  IHL1 : ∀ L2 : list B,
           #|L1| = #|L2|
           → (∀ (n : nat) (x1 : A) (x2 : B),
                n < #|L1|
                → nth_error L1 n = Some x1
                  → nth_error L2 n = Some x2 → P x1 x2) → 
             Forall2 P L1 L2
  b : B
  L2 : list B
  H : S #|L1| = #|b :: L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < S #|L1|
         → nth_error (a :: L1) n = Some x1
           → nth_error (b :: L2) n = Some x2 → P x1 x2
  H2 : #|L1| = #|L2|
  n : nat
  x1 : A
  x2 : B
  H1 : n < #|L1|
  H3 : nth_error L1 n = Some x1
  H4 : nth_error L2 n = Some x2
  ============================
   (S n < S #|L1|)

  
  A : Type
  B : Type
  a : A
  L1 : list A
  P : A → B → Prop
  IHL1 : ∀ L2 : list B,
           #|L1| = #|L2|
           → (∀ (n : nat) (x1 : A) (x2 : B),
                n < #|L1|
                → nth_error L1 n = Some x1
                  → nth_error L2 n = Some x2 → P x1 x2) → 
             Forall2 P L1 L2
  b : B
  L2 : list B
  H : S #|L1| = #|b :: L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < S #|L1|
         → nth_error (a :: L1) n = Some x1
           → nth_error (b :: L2) n = Some x2 → P x1 x2
  H2 : #|L1| = #|L2|
  n : nat
  x1 : A
  x2 : B
  H1 : n < #|L1|
  H3 : nth_error L1 n = Some x1
  H4 : nth_error L2 n = Some x2
  ============================
   (nth_error L1 n = Some x1)

  
  A : Type
  B : Type
  a : A
  L1 : list A
  P : A → B → Prop
  IHL1 : ∀ L2 : list B,
           #|L1| = #|L2|
           → (∀ (n : nat) (x1 : A) (x2 : B),
                n < #|L1|
                → nth_error L1 n = Some x1
                  → nth_error L2 n = Some x2 → P x1 x2) → 
             Forall2 P L1 L2
  b : B
  L2 : list B
  H : S #|L1| = #|b :: L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < S #|L1|
         → nth_error (a :: L1) n = Some x1
           → nth_error (b :: L2) n = Some x2 → P x1 x2
  H2 : #|L1| = #|L2|
  n : nat
  x1 : A
  x2 : B
  H1 : n < #|L1|
  H3 : nth_error L1 n = Some x1
  H4 : nth_error L2 n = Some x2
  ============================
   (nth_error L2 n = Some x2)


DEBUG:Going to execute:
eauto

Goals:
  
  A : Type
  B : Type
  a : A
  L1 : list A
  P : A → B → Prop
  IHL1 : ∀ L2 : list B,
           #|L1| = #|L2|
           → (∀ (n : nat) (x1 : A) (x2 : B),
                n < #|L1|
                → nth_error L1 n = Some x1
                  → nth_error L2 n = Some x2 → P x1 x2) → 
             Forall2 P L1 L2
  b : B
  L2 : list B
  H : S #|L1| = #|b :: L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < S #|L1|
         → nth_error (a :: L1) n = Some x1
           → nth_error (b :: L2) n = Some x2 → P x1 x2
  H2 : #|L1| = #|L2|
  n : nat
  x1 : A
  x2 : B
  H1 : n < #|L1|
  H3 : nth_error L1 n = Some x1
  H4 : nth_error L2 n = Some x2
  ============================
   (S n < S #|L1|)

  
  A : Type
  B : Type
  a : A
  L1 : list A
  P : A → B → Prop
  IHL1 : ∀ L2 : list B,
           #|L1| = #|L2|
           → (∀ (n : nat) (x1 : A) (x2 : B),
                n < #|L1|
                → nth_error L1 n = Some x1
                  → nth_error L2 n = Some x2 → P x1 x2) → 
             Forall2 P L1 L2
  b : B
  L2 : list B
  H : S #|L1| = #|b :: L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < S #|L1|
         → nth_error (a :: L1) n = Some x1
           → nth_error (b :: L2) n = Some x2 → P x1 x2
  H2 : #|L1| = #|L2|
  n : nat
  x1 : A
  x2 : B
  H1 : n < #|L1|
  H3 : nth_error L1 n = Some x1
  H4 : nth_error L2 n = Some x2
  ============================
   (nth_error L1 n = Some x1)

  
  A : Type
  B : Type
  a : A
  L1 : list A
  P : A → B → Prop
  IHL1 : ∀ L2 : list B,
           #|L1| = #|L2|
           → (∀ (n : nat) (x1 : A) (x2 : B),
                n < #|L1|
                → nth_error L1 n = Some x1
                  → nth_error L2 n = Some x2 → P x1 x2) → 
             Forall2 P L1 L2
  b : B
  L2 : list B
  H : S #|L1| = #|b :: L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < S #|L1|
         → nth_error (a :: L1) n = Some x1
           → nth_error (b :: L2) n = Some x2 → P x1 x2
  H2 : #|L1| = #|L2|
  n : nat
  x1 : A
  x2 : B
  H1 : n < #|L1|
  H3 : nth_error L1 n = Some x1
  H4 : nth_error L2 n = Some x2
  ============================
   (nth_error L2 n = Some x2)


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