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),
       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 =>
                  λ (H0 : Some x = Some x1) (H3 : 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 x => x
                                         | None => x
                                         end) H0))))
                          (f_equal (P x1)
                             (f_equal
                                (λ t0 : option B,
                                   match t0 with
                                   | Some x => x
                                   | None => y
                                   end) H3)) in r
              | S n0 =>
                  λ (H0 : nth_error l n0 = Some x1) 
                    (H3 : nth_error l' n0 = Some x2),
                    Forall2_ind
                      (λ (l : list A) (l' : list B),
                         ∀ 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_ind (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) (H : P x y) 
                         (_ : Forall2 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 =>
                             λ (H4 : Some x = Some x1) 
                               (H5 : 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) H4))))
                                     (f_equal (P x1)
                                        (f_equal
                                           (λ t0 : option B,
                                              match t0 with
                                              | Some x0 => x0
                                              | None => y
                                              end) H5)) in H
                         | S n2 =>
                             λ (H4 : nth_error l n2 = Some x1) 
                               (H5 : nth_error l' n2 = Some x2),
                               IHHall n2 H4 H5
                         end) H n0 H0 H3
              end H1 H2)) → Forall2_dep P' (Forall2_cons x y r H))


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

Goals:
  
  A : Type
  B : Type
  P : A → B → Prop
  P' : ∀ (a : A) (b : B), P a b → Prop
  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_ind (P x1 x2)
                        (eq_ind None
                           (λ e : option B,
                              match e with
                              | Some _ => False
                              | None => True
                              end) I (Some x2) H0)
                end H1 H2)
  ============================
   (Forall2_dep P' (Forall2_nil P))

  
  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
  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 =>
                    λ (H0 : Some x = Some x1) (H3 : 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 x => x
                                           | None => x
                                           end) H0))))
                            (f_equal (P x1)
                               (f_equal
                                  (λ t0 : option B,
                                     match t0 with
                                     | Some x => x
                                     | None => y
                                     end) H3)) in r
                | S n0 =>
                    λ (H0 : nth_error l n0 = Some x1) 
                      (H3 : nth_error l' n0 = Some x2),
                      Forall2_ind
                        (λ (l : list A) (l' : list B),
                           ∀ 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_ind (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) (H : P x y) 
                           (_ : Forall2 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 =>
                               λ (H4 : Some x = Some x1) 
                                 (H5 : 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) H4))))
                                       (f_equal (P x1)
                                          (f_equal
                                             (λ t0 : option B,
                                                match t0 with
                                                | Some x0 => x0
                                                | None => y
                                                end) H5)) in H
                           | S n2 =>
                               λ (H4 : nth_error l n2 = Some x1) 
                                 (H5 : nth_error l' n2 = Some x2),
                                 IHHall n2 H4 H5
                           end) H n0 H0 H3
                end H1 H2)
  ============================
   (Forall2_dep P' (Forall2_cons x y r H))


DEBUG:Going to execute:
constructor

Goals:
  
  A : Type
  B : Type
  P : A → B → Prop
  P' : ∀ (a : A) (b : B), P a b → Prop
  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_ind (P x1 x2)
                        (eq_ind None
                           (λ e : option B,
                              match e with
                              | Some _ => False
                              | None => True
                              end) I (Some x2) H0)
                end H1 H2)
  ============================
   (Forall2_dep P' (Forall2_nil P))

  
  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
  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 =>
                    λ (H0 : Some x = Some x1) (H3 : 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 x => x
                                           | None => x
                                           end) H0))))
                            (f_equal (P x1)
                               (f_equal
                                  (λ t0 : option B,
                                     match t0 with
                                     | Some x => x
                                     | None => y
                                     end) H3)) in r
                | S n0 =>
                    λ (H0 : nth_error l n0 = Some x1) 
                      (H3 : nth_error l' n0 = Some x2),
                      Forall2_ind
                        (λ (l : list A) (l' : list B),
                           ∀ 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_ind (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) (H : P x y) 
                           (_ : Forall2 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 =>
                               λ (H4 : Some x = Some x1) 
                                 (H5 : 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) H4))))
                                       (f_equal (P x1)
                                          (f_equal
                                             (λ t0 : option B,
                                                match t0 with
                                                | Some x0 => x0
                                                | None => y
                                                end) H5)) in H
                           | S n2 =>
                               λ (H4 : nth_error l n2 = Some x1) 
                                 (H5 : nth_error l' n2 = Some x2),
                                 IHHall n2 H4 H5
                           end) H n0 H0 H3
                end H1 H2)
  ============================
   (Forall2_dep P' (Forall2_cons x y r H))


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>