Goal:
  
  A : Type
  B : Type
  L1 : list A
  L2 : list B
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  H : All2 P L1 L2
  ============================
   ((∀ (n : nat) (x1 : A) (x2 : B),
       n < #|L1|
       → ∀ (H1 : nth_error L1 n = Some x1) (H2 : nth_error L2 n = Some x2),
           P' x1 x2 (All2_nth_error n x1 x2 H H1 H2)) → 
    All2_dep P' H)


DEBUG:Going to execute:
induction H; cbn; intro H'