Goal:
  
  A : Type
  P : list A → list A → A → A → Type
  Γ : list A
  Γ' : list A
  a : A
  Δ : list A
  a0 : A
  Δ' : list A
  H : S #|Δ| = S #|Δ'|
  IHΔ : All2_fold P (Δ ++ Γ) (Δ' ++ Γ')
        → All2_fold P Γ Γ'
          × All2_fold (λ Δ Δ' : list A, P (Δ ++ Γ) (Δ' ++ Γ')) Δ Δ'
  H' : All2_fold P ((a :: Δ) ++ Γ) ((a0 :: Δ') ++ Γ')
  ============================
   (All2_fold P Γ Γ'
    × All2_fold (λ Δ Δ' : list A, P (Δ ++ Γ) (Δ' ++ Γ')) (a :: Δ) (a0 :: Δ'))


DEBUG:Going to execute:
depelim H'; specialize (IHΔ H')
DEBUG LTAC Evaluated term: (IHΔ Γ Γ' Δ'
                              (ZifyClasses.rew_iff_rev 
                                 (#|Δ| = #|Δ'|)
                                 (BinInt.Z.of_nat #|Δ| =
                                  BinInt.Z.of_nat #|Δ'|)
                                 (ZifyClasses.mkrel nat BinNums.Z eq
                                    BinInt.Z.of_nat eq
                                    (λ x y : nat,
                                       iff_sym (Znat.Nat2Z.inj_iff x y)) #|Δ|
                                    (BinInt.Z.of_nat #|Δ|) eq_refl #|Δ'|
                                    (BinInt.Z.of_nat #|Δ'|) eq_refl)
                                 (let H0 :
                                    BinInt.Z.add (BinInt.Z.of_nat #|Δ|)
                                      (BinNums.Zpos BinNums.xH) =
                                    BinInt.Z.add (BinInt.Z.of_nat #|Δ'|)
                                      (BinNums.Zpos BinNums.xH) :=
                                    ZifyClasses.rew_iff 
                                      (S #|Δ| = S #|Δ'|)
                                      (BinInt.Z.add 
                                         (BinInt.Z.of_nat #|Δ|)
                                         (BinNums.Zpos BinNums.xH) =
                                       BinInt.Z.add 
                                         (BinInt.Z.of_nat #|Δ'|)
                                         (BinNums.Zpos BinNums.xH))
                                      (ZifyClasses.mkrel nat BinNums.Z eq
                                         BinInt.Z.of_nat eq
                                         (λ x y : nat,
                                            iff_sym (Znat.Nat2Z.inj_iff x y))
                                         (S #|Δ|)
                                         ((λ x : BinNums.Z,
                                             BinInt.Z.add x
                                               (BinNums.Zpos BinNums.xH))
                                            (BinInt.Z.of_nat #|Δ|))
                                         (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 #|Δ|
                                            (BinInt.Z.of_nat #|Δ|) eq_refl)
                                         (S #|Δ'|)
                                         ((λ x : BinNums.Z,
                                             BinInt.Z.add x
                                               (BinNums.Zpos BinNums.xH))
                                            (BinInt.Z.of_nat #|Δ'|))
                                         (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 #|Δ'|
                                            (BinInt.Z.of_nat #|Δ'|) eq_refl))
                                      H in
                                  let cstr :
                                    BinInt.Z.le BinNums.Z0
                                      (BinInt.Z.of_nat #|Δ'|) :=
                                    Znat.Nat2Z.is_nonneg #|Δ'| in
                                  let cstr0 :
                                    BinInt.Z.le BinNums.Z0
                                      (BinInt.Z.of_nat #|Δ|) :=
                                    Znat.Nat2Z.is_nonneg #|Δ| in
                                  let __arith :
                                    ∀ __x2 __x1 : BinNums.Z,
                                      BinInt.Z.add __x1
                                        (BinNums.Zpos BinNums.xH) =
                                      BinInt.Z.add __x2
                                        (BinNums.Zpos BinNums.xH)
                                      → __x1 = __x2 :=
                                    λ __x2 __x1 : BinNums.Z,
                                      let __wit :=
                                        [ZMicromega.RatProof
                                           (RingMicromega.PsatzAdd
                                              (RingMicromega.PsatzMulC
                                                 (EnvRing.Pc
                                                 (BinNums.Zneg BinNums.xH))
                                                 (RingMicromega.PsatzIn
                                                 BinNums.Z 1))
                                              (RingMicromega.PsatzIn
                                                 BinNums.Z 0))
                                           ZMicromega.DoneProof] in
                                      let __varmap :=
                                        VarMap.Branch 
                                          (VarMap.Elt __x2) __x1 VarMap.Empty
                                        in
                                      let __ff :=
                                        Tauto.IMPL
                                          (Tauto.A Tauto.isProp
                                             {|
                                               RingMicromega.Flhs :=
                                                 EnvRing.PEadd
                                                 (EnvRing.PEX BinNums.xH)
                                                 (EnvRing.PEc
                                                 (BinNums.Zpos BinNums.xH));
                                               RingMicromega.Fop :=
                                                 RingMicromega.OpEq;
                                               RingMicromega.Frhs :=
                                                 EnvRing.PEadd
                                                 (EnvRing.PEX
                                                 (BinNums.xO BinNums.xH))
                                                 (EnvRing.PEc
                                                 (BinNums.Zpos BinNums.xH))
                                             |} tt) None
                                          (Tauto.A Tauto.isProp
                                             {|
                                               RingMicromega.Flhs :=
                                                 EnvRing.PEX BinNums.xH;
                                               RingMicromega.Fop :=
                                                 RingMicromega.OpEq;
                                               RingMicromega.Frhs :=
                                                 EnvRing.PEX
                                                 (BinNums.xO 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 #|Δ'|)
                                    (BinInt.Z.of_nat #|Δ|) H0)))