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


DEBUG:Going to execute:
cbn in H'
DEBUG LTAC Evaluated term: (H' 0 x y
                              (ZifyClasses.rew_iff_rev 
                                 (0 < S #|l|)
                                 (BinInt.Z.lt BinNums.Z0
                                    (BinInt.Z.add 
                                       (BinInt.Z.of_nat #|l|)
                                       (BinNums.Zpos BinNums.xH)))
                                 (ZifyClasses.mkrel nat BinNums.Z lt
                                    BinInt.Z.of_nat BinInt.Z.lt
                                    Znat.Nat2Z.inj_lt 0 BinNums.Z0 eq_refl
                                    (S #|l|)
                                    (BinInt.Z.add 
                                       (BinInt.Z.of_nat #|l|)
                                       (BinNums.Zpos BinNums.xH))
                                    (ZifyClasses.mkapp nat nat BinNums.Z
                                       BinNums.Z S BinInt.Z.of_nat
                                       BinInt.Z.of_nat
                                       (λ x : BinNums.Z,
                                          BinInt.Z.add x
                                            (BinNums.Zpos BinNums.xH))
                                       Znat.Nat2Z.inj_succ #|l|
                                       (BinInt.Z.of_nat #|l|) eq_refl))
                                 (let cstr :
                                    BinInt.Z.le BinNums.Z0
                                      (BinInt.Z.of_nat #|l|) :=
                                    Znat.Nat2Z.is_nonneg #|l| in
                                  let __arith :
                                    ∀ __x1 : BinNums.Z,
                                      BinInt.Z.le BinNums.Z0 __x1
                                      → BinInt.Z.lt BinNums.Z0
                                          (BinInt.Z.add __x1
                                             (BinNums.Zpos BinNums.xH)) :=
                                    λ __x1 : BinNums.Z,
                                      let __wit := [] in
                                      let __varmap := VarMap.Elt __x1 in
                                      let __ff :=
                                        Tauto.IMPL
                                          (Tauto.A Tauto.isProp
                                             {|
                                               RingMicromega.Flhs :=
                                                 EnvRing.PEc BinNums.Z0;
                                               RingMicromega.Fop :=
                                                 RingMicromega.OpLe;
                                               RingMicromega.Frhs :=
                                                 EnvRing.PEX BinNums.xH
                                             |} tt) None
                                          (Tauto.A Tauto.isProp
                                             {|
                                               RingMicromega.Flhs :=
                                                 EnvRing.PEc BinNums.Z0;
                                               RingMicromega.Fop :=
                                                 RingMicromega.OpLt;
                                               RingMicromega.Frhs :=
                                                 EnvRing.PEadd
                                                 (EnvRing.PEX BinNums.xH)
                                                 (EnvRing.PEc
                                                 (BinNums.Zpos BinNums.xH))
                                             |} tt) in
                                      ZMicromega.ZTautoChecker_sound __ff
                                        __wit
                                        (eq_refl
                                         <:
                                         ZMicromega.ZTautoChecker __ff __wit =
                                         true)
                                        (VarMap.find BinNums.Z0 __varmap) in
                                  __arith (BinInt.Z.of_nat #|l|) cstr))
                              eq_refl eq_refl)