Goal:
  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  l : list A
  l' : list B
  t : A
  t' : B
  H : All2 P l l'
  H' : All2_dep P' H
  ============================
   (∀ (n : nat) (H1 : nth_error l n = Some t) (H2 : nth_error l' n = Some t'),
      P' t t' (All2_nth_error n t t' H H1 H2))


DEBUG:Going to execute:
induction H'

Goals:
  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  t : A
  t' : B
  ============================
   (∀ (n : nat) (H1 : nth_error [] n = Some t) (H2 : 
                                                nth_error [] n = Some t'),
      P' t t' (All2_nth_error n t t' All2_nil H1 H2))

  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  t : A
  t' : B
  x : A
  y : B
  l : list A
  l' : list B
  r : P x y
  rs : All2 P l l'
  r0 : P' x y r
  H' : All2_dep P' rs
  IHH' : ∀ (n : nat) (H1 : nth_error l n = Some t) 
           (H2 : nth_error l' n = Some t'),
           P' t t' (All2_nth_error n t t' rs H1 H2)
  ============================
   (∀ (n : nat) (H1 : nth_error (x :: l) n = Some t) 
      (H2 : nth_error (y :: l') n = Some t'),
      P' t t' (All2_nth_error n t t' (All2_cons r rs) H1 H2))


DEBUG:Going to execute:
destruct n
DEBUG LTAC Evaluated term: H'

Goals:
  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  t : A
  t' : B
  ============================
   (∀ (H1 : nth_error [] 0 = Some t) (H2 : nth_error [] 0 = Some t'),
      P' t t' (All2_nth_error 0 t t' All2_nil H1 H2))

  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  t : A
  t' : B
  n : nat
  ============================
   (∀ (H1 : nth_error [] (S n) = Some t) (H2 : nth_error [] (S n) = Some t'),
      P' t t' (All2_nth_error (S n) t t' All2_nil H1 H2))

  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  t : A
  t' : B
  x : A
  y : B
  l : list A
  l' : list B
  r : P x y
  rs : All2 P l l'
  r0 : P' x y r
  H' : All2_dep P' rs
  IHH' : ∀ (n : nat) (H1 : nth_error l n = Some t) 
           (H2 : nth_error l' n = Some t'),
           P' t t' (All2_nth_error n t t' rs H1 H2)
  ============================
   (∀ (H1 : nth_error (x :: l) 0 = Some t) (H2 : nth_error (y :: l') 0 =
                                                 Some t'),
      P' t t' (All2_nth_error 0 t t' (All2_cons r rs) H1 H2))

  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  t : A
  t' : B
  x : A
  y : B
  l : list A
  l' : list B
  r : P x y
  rs : All2 P l l'
  r0 : P' x y r
  H' : All2_dep P' rs
  IHH' : ∀ (n : nat) (H1 : nth_error l n = Some t) 
           (H2 : nth_error l' n = Some t'),
           P' t t' (All2_nth_error n t t' rs H1 H2)
  n : nat
  ============================
   (∀ (H1 : nth_error (x :: l) (S n) = Some t) (H2 : 
                                                nth_error (y :: l') (S n) =
                                                Some t'),
      P' t t' (All2_nth_error (S n) t t' (All2_cons r rs) H1 H2))


DEBUG:Going to execute:
cbn

Goals:
  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  t : A
  t' : B
  ============================
   (None = Some t
    → ∀ H2 : None = Some t',
        P' t t'
          (False_rect (P t t')
             (eq_ind None
                (λ e : option B,
                   match e with
                   | Some _ => False
                   | None => True
                   end) I (Some t') H2)))

  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  t : A
  t' : B
  n : nat
  ============================
   (None = Some t
    → ∀ H2 : None = Some t',
        P' t t'
          (False_rect (P t t')
             (eq_ind None
                (λ e : option B,
                   match e with
                   | Some _ => False
                   | None => True
                   end) I (Some t') H2)))

  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  t : A
  t' : B
  x : A
  y : B
  l : list A
  l' : list B
  r : P x y
  rs : All2 P l l'
  r0 : P' x y r
  H' : All2_dep P' rs
  IHH' : ∀ (n : nat) (H1 : nth_error l n = Some t) 
           (H2 : nth_error l' n = Some t'),
           P' t t' (All2_nth_error n t t' rs H1 H2)
  ============================
   (∀ (H1 : Some x = Some t) (H2 : Some y = Some t'),
      P' t t'
        (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) H1))))
               (f_equal (P t)
                  (f_equal
                     (λ t0 : option B,
                        match t0 with
                        | Some x => x
                        | None => y
                        end) H2)) in r))

  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  t : A
  t' : B
  x : A
  y : B
  l : list A
  l' : list B
  r : P x y
  rs : All2 P l l'
  r0 : P' x y r
  H' : All2_dep P' rs
  IHH' : ∀ (n : nat) (H1 : nth_error l n = Some t) 
           (H2 : nth_error l' n = Some t'),
           P' t t' (All2_nth_error n t t' rs H1 H2)
  n : nat
  ============================
   (∀ (H1 : nth_error l n = Some t) (H2 : nth_error l' n = Some t'),
      P' t t'
        (All2_rect A B P
           (λ (l : list A) (l' : list B) (_ : All2 P l l'),
              ∀ n : nat,
                nth_error l n = Some t → nth_error l' n = Some t' → P t t')
           (λ n : nat,
              match
                n as n0
                return
                  (nth_error [] n0 = Some t
                   → nth_error [] n0 = Some t' → P t t')
              with
              | 0 | _ =>
                  λ (_ : None = Some t) (H0 : None = Some t'),
                    False_rect (P t t')
                      (eq_ind None
                         (λ e : option B,
                            match e with
                            | Some _ => False
                            | None => True
                            end) I (Some t') H0)
              end)
           (λ (x : A) (y : B) (l : list A) (l' : list B) 
              (r : P x y) (_ : All2 P l l') (IHHall : 
                                             ∀ n : nat,
                                               nth_error l n = Some t
                                               → nth_error l' n = Some t'
                                                 → 
                                                 P t t') 
              (n : nat),
              match
                n as n0
                return
                  (nth_error (x :: l) n0 = Some t
                   → nth_error (y :: l') n0 = Some t' → P t t')
              with
              | 0 =>
                  λ (H : Some x = Some t) (H0 : Some y = Some t'),
                    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 t)
                             (f_equal
                                (λ t0 : option B,
                                   match t0 with
                                   | Some x0 => x0
                                   | None => y
                                   end) H0)) in r
              | S n0 =>
                  λ (H : nth_error l n0 = Some t) 
                    (H0 : nth_error l' n0 = Some t'), 
                    IHHall n0 H H0
              end) l l' rs n H1 H2))


DEBUG:Going to execute:
try congruence