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


DEBUG:Going to execute:
cbn in H'
DEBUG LTAC Evaluated term: (H' (S n) x1 x2
                              (ZifyClasses.rew_iff_rev 
                                 (S n < S #|l|)
                                 (BinInt.Z.lt
                                    (BinInt.Z.add 
                                       (BinInt.Z.of_nat n)
                                       (BinNums.Zpos BinNums.xH))
                                    (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 
                                    (S n)
                                    (BinInt.Z.add 
                                       (BinInt.Z.of_nat n)
                                       (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 n
                                       (BinInt.Z.of_nat n) 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 Hn0 :
                                    BinInt.Z.lt (BinInt.Z.of_nat n)
                                      (BinInt.Z.of_nat #|l|) :=
                                    ZifyClasses.rew_iff 
                                      (n < #|l|)
                                      (BinInt.Z.lt 
                                         (BinInt.Z.of_nat n)
                                         (BinInt.Z.of_nat #|l|))
                                      (ZifyClasses.mkrel nat BinNums.Z lt
                                         BinInt.Z.of_nat BinInt.Z.lt
                                         Znat.Nat2Z.inj_lt n
                                         (BinInt.Z.of_nat n) eq_refl #|l|
                                         (BinInt.Z.of_nat #|l|) eq_refl) Hn
                                    in
                                  let cstr :
                                    BinInt.Z.le BinNums.Z0
                                      (BinInt.Z.of_nat n) :=
                                    Znat.Nat2Z.is_nonneg n in
                                  let cstr0 :
                                    BinInt.Z.le BinNums.Z0
                                      (BinInt.Z.of_nat #|l|) :=
                                    Znat.Nat2Z.is_nonneg #|l| in
                                  let __arith :
                                    ∀ __x2 __x1 : BinNums.Z,
                                      BinInt.Z.lt __x1 __x2
                                      → BinInt.Z.lt
                                          (BinInt.Z.add __x1
                                             (BinNums.Zpos BinNums.xH))
                                          (BinInt.Z.add __x2
                                             (BinNums.Zpos BinNums.xH)) :=
                                    λ __x2 __x1 : BinNums.Z,
                                      let __wit := [] in
                                      let __varmap :=
                                        VarMap.Branch 
                                          (VarMap.Elt __x2) __x1 VarMap.Empty
                                        in
                                      let __ff :=
                                        Tauto.IMPL
                                          (Tauto.A Tauto.isProp
                                             {|
                                               RingMicromega.Flhs :=
                                                 EnvRing.PEX BinNums.xH;
                                               RingMicromega.Fop :=
                                                 RingMicromega.OpLt;
                                               RingMicromega.Frhs :=
                                                 EnvRing.PEX
                                                 (BinNums.xO BinNums.xH)
                                             |} tt) None
                                          (Tauto.A Tauto.isProp
                                             {|
                                               RingMicromega.Flhs :=
                                                 EnvRing.PEadd
                                                 (EnvRing.PEX BinNums.xH)
                                                 (EnvRing.PEc
                                                 (BinNums.Zpos BinNums.xH));
                                               RingMicromega.Fop :=
                                                 RingMicromega.OpLt;
                                               RingMicromega.Frhs :=
                                                 EnvRing.PEadd
                                                 (EnvRing.PEX
                                                 (BinNums.xO 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|)
                                    (BinInt.Z.of_nat n) Hn0)) H1 H2)