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),
       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:
<coq-core.plugins.ltac::intro@1> $1

Goals:
  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  H' : ∀ (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
  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:
constructor

Goals:
  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  H' : ∀ (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
  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:
<coq-core.plugins.ltac::constructor@0>