Goal:
  
  A : Type
  B : Type
  L1 : list A
  L2 : list B
  P : A → B → Prop
  P' : ∀ (a : A) (b : B), P a b → Prop
  H : Forall2 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 (Forall2_nth_error n x1 x2 H H1 H2)) → 
    Forall2_dep P' H)


DEBUG:Going to execute:
induction H using Forall2_rect; cbn