Goal:
  
  A : Type
  B : Type
  P : A → B → Type
  H : 0 = #|[]|
  X : ∀ (n : nat) (x1 : A) (x2 : B),
        n < 0 → nth_error [] n = Some x1 → nth_error [] n = Some x2 → P x1 x2
  ============================
   (All2 P [] [])


DEBUG:Going to execute:
inversion_clear H
DEBUG LTAC Evaluated term: H
DEBUG LTAC Evaluated term: H
DEBUG LTAC Evaluated term: H
DEBUG LTAC Evaluated term: H