Goal:
  
  A : Type
  P : list A → list A → A → A → Type
  Γ : list A
  Γ' : list A
  a : A
  Δ : list A
  a0 : A
  Δ' : list A
  H : #|Γ| = #|Γ'|
  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.of_nat #|Γ| =
                                    BinInt.Z.of_nat #|Γ'| :=
                                    ZifyClasses.rew_iff 
                                      (#|Γ| = #|Γ'|)
                                      (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) 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,
                                      __x1 = __x2 → __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.PEX BinNums.xH;
                                               RingMicromega.Fop :=
                                                 RingMicromega.OpEq;
                                               RingMicromega.Frhs :=
                                                 EnvRing.PEX
                                                 (BinNums.xO 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)))