Goal:
  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : P x y
  H : All2 P l l'
  IHAll2 : (∀ (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 (All2_nth_error n x1 x2 H H1 H2)) → 
           All2_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
         (All2_rect A B P
            (λ (l : list A) (l' : list B) (_ : All2 P l l'),
               ∀ 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_rect (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) 
               (r : P x y) (_ : All2 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 =>
                   λ (H : Some x = Some x1) (H0 : Some y = Some x2),
                     rew [λ X : Type, X]
                         eq_trans
                           (f_equal (λ f : B → Type, f y)
                              (eq_trans eq_refl
                                 (f_equal P
                                    (f_equal
                                       (λ t0 : option A,
                                          match t0 with
                                          | Some x0 => x0
                                          | None => x
                                          end) H))))
                           (f_equal (P x1)
                              (f_equal
                                 (λ t0 : option B,
                                    match t0 with
                                    | Some x0 => x0
                                    | None => y
                                    end) H0)) in r
               | S n0 =>
                   λ (H : nth_error l n0 = Some x1) 
                     (H0 : nth_error l' n0 = Some x2), 
                     IHHall n0 H H0
               end) l l' H n H1 H2)
  Hn : n < #|l|
  ============================
   (P' x1 x2 (All2_nth_error n x1 x2 H H1 H2))


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