Goal:
  
  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:
congruence
Level 0: Backtrace:

Tactic failure: congruence failed.
Level 0: Backtrace:

Tactic failure: congruence failed.