Goal:
  
  A : Type
  B : Type
  P : A → B → Prop
  L2 : list B
  H : 0 = #|L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < 0
         → nth_error [] n = Some x1 → nth_error L2 n = Some x2 → P x1 x2
  ============================
   (Forall2 P [] L2)


DEBUG:Going to execute:
destruct L2

Goals:
  
  A : Type
  B : Type
  P : A → B → Prop
  H : 0 = #|[]|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < 0
         → nth_error [] n = Some x1 → nth_error [] n = Some x2 → P x1 x2
  ============================
   (Forall2 P [] [])

  
  A : Type
  B : Type
  P : A → B → Prop
  b : B
  L2 : list B
  H : 0 = #|b :: L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < 0
         → nth_error [] n = Some x1
           → nth_error (b :: L2) n = Some x2 → P x1 x2
  ============================
   (Forall2 P [] (b :: L2))


DEBUG:Going to execute:
inv H
DEBUG LTAC Evaluated term: L2

Goals:
  
  A : Type
  B : Type
  P : A → B → Prop
  H : 0 = #|[]|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < 0
         → nth_error [] n = Some x1 → nth_error [] n = Some x2 → P x1 x2
  ============================
   (Forall2 P [] [])

  
  A : Type
  B : Type
  P : A → B → Prop
  b : B
  L2 : list B
  H : 0 = #|b :: L2|
  H0 : ∀ (n : nat) (x1 : A) (x2 : B),
         n < 0
         → nth_error [] n = Some x1
           → nth_error (b :: L2) n = Some x2 → P x1 x2
  ============================
   (Forall2 P [] (b :: L2))


DEBUG:Going to execute:
fun H => inversion_clear H