Goal:
  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  l : list A
  l' : list B
  n : nat
  t : A
  t' : B
  H : All2 P l l'
  H' : All2_dep P' H
  H1 : nth_error l n = Some t
  H2 : nth_error l' n = Some t'
  ============================
   (P' t t' (All2_nth_error n t t' H H1 H2))


DEBUG:Going to execute:
generalize dependent n; induction H'; destruct n