Goal:
  
  A : Type
  B : Type
  P : A → B → Type
  P' : ∀ (a : A) (b : B), P a b → Type
  ============================
   ((∀ (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_rect (P x1 x2)
                      (eq_ind None
                         (λ e : option B,
                            match e with
                            | Some _ => False
                            | None => True
                            end) I (Some x2) H0)
              end H1 H2)) → All2_dep P' All2_nil)


DEBUG:Going to execute:
<coq-core.plugins.ltac::intro@1> $1