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)
  ============================
   (∀ (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))


DEBUG:Going to execute:
congruence