Goal:
  
  A : Type
  B : Type
  P : A → B → Prop
  P' : ∀ (a : A) (b : B), P a b → Prop
  x : A
  y : B
  l : list A
  l' : list B
  r : P x y
  H : Forall2 P l l'
  IHForall2 : (∀ (n : nat) (x1 : A) (x2 : B),
                 n < #|l|
                 → ∀ (H1 : nth_error l n = Some x1) 
                     (H2 : nth_error l' n = Some x2),
                     P' x1 x2 (Forall2_nth_error n x1 x2 H H1 H2))
              → Forall2_dep P' H
  n : nat
  x1 : A
  x2 : B
  H1 : nth_error l n = Some x1
  H2 : nth_error l' n = Some x2
  H' : P' x1 x2
         (Forall2_ind
            (λ (l : list A) (l' : list B),
               ∀ n : nat,
                 nth_error l n = Some x1 → nth_error l' n = Some x2 → P x1 x2)
            (λ n : nat,
               match
                 n as n0
                 return
                   (nth_error [] n0 = Some x1
                    → nth_error [] n0 = Some x2 → P x1 x2)
               with
               | 0 | _ =>
                   λ (_ : None = Some x1) (H0 : None = Some x2),
                     False_ind (P x1 x2)
                       (eq_ind None
                          (λ e : option B,
                             match e with
                             | Some _ => False
                             | None => True
                             end) I (Some x2) H0)
               end)
            (λ (x : A) (y : B) (l : list A) (l' : list B) 
               (H : P x y) (_ : Forall2 P l l') (IHHall : 
                                                 ∀ n : nat,
                                                 nth_error l n = Some x1
                                                 → 
                                                 nth_error l' n = Some x2
                                                 → 
                                                 P x1 x2) 
               (n : nat),
               match
                 n as n0
                 return
                   (nth_error (x :: l) n0 = Some x1
                    → nth_error (y :: l') n0 = Some x2 → P x1 x2)
               with
               | 0 =>
                   λ (H0 : Some x = Some x1) (H1 : Some y = Some x2),
                     rew [λ X : Prop, X]
                         eq_trans
                           (f_equal (λ f : B → Prop, f y)
                              (eq_trans eq_refl
                                 (f_equal P
                                    (f_equal
                                       (λ t0 : option A,
                                          match t0 with
                                          | Some x0 => x0
                                          | None => x
                                          end) H0))))
                           (f_equal (P x1)
                              (f_equal
                                 (λ t0 : option B,
                                    match t0 with
                                    | Some x0 => x0
                                    | None => y
                                    end) H1)) in H
               | S n0 =>
                   λ (H0 : nth_error l n0 = Some x1) 
                     (H1 : nth_error l' n0 = Some x2), 
                     IHHall n0 H0 H1
               end) H n H1 H2)
  Hn : n < #|l|
  ============================
   (P' x1 x2 (Forall2_nth_error n x1 x2 H H1 H2))


DEBUG:Going to execute:
<coq-core.plugins.ltac::exact@0> $1