Goal:
  
  A : Type
  B : Type
  P : A → B → Prop
  P' : ∀ (a : A) (b : B), P a b → Prop
  t : A
  t' : B
  y : B
  l : list A
  l' : list B
  r : P t y
  rs : Forall2 P l l'
  H : P' t y r
  H' : Forall2_dep P' rs
  IHH' : ∀ (n : nat) (H1 : nth_error l n = Some t) 
           (H2 : nth_error l' n = Some t'),
           P' t t' (Forall2_nth_error n t t' rs H1 H2)
  H2 : Some y = Some t'
  k : (λ t0 : option B, match t0 with
                        | Some x => x
                        | None => y
                        end) (Some y) =
      (λ t0 : option B, match t0 with
                        | Some x => x
                        | None => y
                        end) (Some t')
  ============================
   (P' t t'
      (rew [λ X : Prop, X]
           eq_trans
             (f_equal (λ f : B → Prop, f y)
                (eq_trans eq_refl (f_equal P eq_refl))) 
             (f_equal (P t) k) in r))


DEBUG:Going to execute:
cbn in k