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
  H' : ∀ (n : nat) (x1 : A) (x2 : B),
         n < S #|l|
         → ∀ (H1 : nth_error (x :: l) n = Some x1) 
             (H2 : nth_error (y :: l') n = Some x2),
             P' x1 x2
               (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 x => x
                                           | None => x
                                           end) H))))
                            (f_equal (P x1)
                               (f_equal
                                  (λ t0 : option B,
                                     match t0 with
                                     | Some x => x
                                     | None => y
                                     end) H0)) in r
                | S n0 =>
                    λ (H0 : nth_error l n0 = Some x1) 
                      (H3 : nth_error l' n0 = Some x2),
                      All2_rect A B P
                        (λ (l : list A) (l' : list B) (_ : All2 P l l'),
                           ∀ n1 : nat,
                             nth_error l n1 = Some x1
                             → nth_error l' n1 = Some x2 → P x1 x2)
                        (λ n1 : nat,
                           match
                             n1 as n2
                             return
                               (nth_error [] n2 = Some x1
                                → nth_error [] n2 = Some x2 → P x1 x2)
                           with
                           | 0 | _ =>
                               λ (_ : None = Some x1) (H4 : 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) H4)
                           end)
                        (λ (x : A) (y : B) (l : list A) 
                           (l' : list B) (r : P x y) 
                           (_ : All2 P l l') (IHHall : 
                                              ∀ n1 : nat,
                                                nth_error l n1 = Some x1
                                                → 
                                                nth_error l' n1 = Some x2
                                                → 
                                                P x1 x2) 
                           (n1 : nat),
                           match
                             n1 as n2
                             return
                               (nth_error (x :: l) n2 = Some x1
                                → nth_error (y :: l') n2 = Some x2 → P x1 x2)
                           with
                           | 0 =>
                               λ (H : Some x = Some x1) 
                                 (H4 : 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) H4)) in r
                           | S n2 =>
                               λ (H : nth_error l n2 = Some x1) 
                                 (H4 : nth_error l' n2 = Some x2),
                                 IHHall n2 H H4
                           end) l l' H n0 H0 H3
                end H1 H2)
  ============================
   (0 < S #|l|)


DEBUG:Going to execute:
idtac