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

Goals:
  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  ============================
   ((∀ (n : nat) (x1 : A) (x2 : B),
       n < #|[]|
       → ∀ (H1 : nth_error [] n = Some x1) (H2 : nth_error [] n = Some x2),
           P' x1 x2 (All2_nth_error n x1 x2 All2_nil H1 H2))
    → All2_dep P' All2_nil)

  
  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),
       n < #|x :: l|
       → ∀ (H1 : nth_error (x :: l) n = Some x1) (H2 : 
                                                 nth_error (y :: l') n =
                                                 Some x2),
           P' x1 x2 (All2_nth_error n x1 x2 (All2_cons r H) H1 H2))
    → All2_dep P' (All2_cons r H))


DEBUG:Going to execute:
cbn
DEBUG LTAC Evaluated term: H

Goals:
  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  ============================
   ((∀ (n : nat) (x1 : A) (x2 : B),
       n < 0
       → ∀ (H1 : nth_error [] n = Some x1) (H2 : nth_error [] n = Some x2),
           P' x1 x2
             (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 H1 H2)) → All2_dep P' All2_nil)

  
  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),
       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)) → All2_dep P' (All2_cons r H))


DEBUG:Going to execute:
intro H'