Goal:
  
  A : Type
  B : Type
  L1 : list A
  L2 : list B
  P : A → B → Prop
  P' : ∀ (a : A) (b : B), P a b → Prop
  H : Forall2 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 (Forall2_nth_error n x1 x2 H H1 H2)) → 
    Forall2_dep P' H)


DEBUG:Going to execute:
induction H using Forall2_rect

Goals:
  
  A : Type
  B : Type
  P : A → B → Prop
  P' : ∀ (a : A) (b : B), P a b → Prop
  ============================
   ((∀ (n : nat) (x1 : A) (x2 : B),
       n < #|[]|
       → ∀ (H1 : nth_error [] n = Some x1) (H2 : nth_error [] n = Some x2),
           P' x1 x2 (Forall2_nth_error n x1 x2 (Forall2_nil P) 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
  ============================
   ((∀ (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 (Forall2_nth_error n x1 x2 (Forall2_cons x y r H) H1 H2))
    → Forall2_dep P' (Forall2_cons x y r H))


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

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