Goal:
  
  A : Type
  B : Type
  P : A → B → Prop
  n : nat
  x : A
  l : list A
  e : nth_error l n = None
  y : B
  l' : list B
  H : P x y
  h : Forall2 P l l'
  IHn : ∀ (l : list A) (l' : list B),
          nth_error l n = None → Forall2 P l l' → nth_error l' n = None
  ============================
   (nth_error l' n = None)


DEBUG:Going to execute:
eapply IHn

Goals:
  
  A : Type
  B : Type
  P : A → B → Prop
  n : nat
  x : A
  l : list A
  e : nth_error l n = None
  y : B
  l' : list B
  H : P x y
  h : Forall2 P l l'
  IHn : ∀ (l : list A) (l' : list B),
          nth_error l n = None → Forall2 P l l' → nth_error l' n = None
  ============================
   (nth_error ?l n = None)

  
  A : Type
  B : Type
  P : A → B → Prop
  n : nat
  x : A
  l : list A
  e : nth_error l n = None
  y : B
  l' : list B
  H : P x y
  h : Forall2 P l l'
  IHn : ∀ (l : list A) (l' : list B),
          nth_error l n = None → Forall2 P l l' → nth_error l' n = None
  ============================
   (Forall2 P ?l l')


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

Goals:
  
  A : Type
  B : Type
  P : A → B → Prop
  n : nat
  x : A
  l : list A
  e : nth_error l n = None
  y : B
  l' : list B
  H : P x y
  h : Forall2 P l l'
  IHn : ∀ (l : list A) (l' : list B),
          nth_error l n = None → Forall2 P l l' → nth_error l' n = None
  ============================
   (nth_error ?l n = None)

  
  A : Type
  B : Type
  P : A → B → Prop
  n : nat
  x : A
  l : list A
  e : nth_error l n = None
  y : B
  l' : list B
  H : P x y
  h : Forall2 P l l'
  IHn : ∀ (l : list A) (l' : list B),
          nth_error l n = None → Forall2 P l l' → nth_error l' n = None
  ============================
   (Forall2 P ?l l')


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