Goal:
  
  A : Type
  B : Type
  P : nat → A → B → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : P #|l| x y
  X : All2i_len P l l'
  IHX : BinInt.Z.of_nat #|l| = BinInt.Z.of_nat #|l'|
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l'|)
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH) =
    BinInt.Z.add (BinInt.Z.of_nat #|l'|) (BinNums.Zpos BinNums.xH))


DEBUG:Going to execute:
idtac

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (BinNums.Z0 = BinNums.Z0)

  
  A : Type
  B : Type
  P : nat → A → B → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : P #|l| x y
  X : All2i_len P l l'
  IHX : BinInt.Z.of_nat #|l| = BinInt.Z.of_nat #|l'|
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l'|)
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH) =
    BinInt.Z.add (BinInt.Z.of_nat #|l'|) (BinNums.Zpos BinNums.xH))


DEBUG:Going to execute:
Zify.zify_post_hook

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (BinNums.Z0 = BinNums.Z0)

  
  A : Type
  B : Type
  P : nat → A → B → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : P #|l| x y
  X : All2i_len P l l'
  IHX : BinInt.Z.of_nat #|l| = BinInt.Z.of_nat #|l'|
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l'|)
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH) =
    BinInt.Z.add (BinInt.Z.of_nat #|l'|) (BinNums.Zpos BinNums.xH))


DEBUG:Going to execute:
idtac

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (BinNums.Z0 = BinNums.Z0)

  
  A : Type
  B : Type
  P : nat → A → B → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : P #|l| x y
  X : All2i_len P l l'
  IHX : BinInt.Z.of_nat #|l| = BinInt.Z.of_nat #|l'|
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l'|)
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH) =
    BinInt.Z.add (BinInt.Z.of_nat #|l'|) (BinNums.Zpos BinNums.xH))


DEBUG:Going to execute:
zify_saturate

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (BinNums.Z0 = BinNums.Z0)

  
  A : Type
  B : Type
  P : nat → A → B → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : P #|l| x y
  X : All2i_len P l l'
  IHX : BinInt.Z.of_nat #|l| = BinInt.Z.of_nat #|l'|
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l'|)
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH) =
    BinInt.Z.add (BinInt.Z.of_nat #|l'|) (BinNums.Zpos BinNums.xH))


DEBUG:Going to execute:
<coq-core.plugins.zify::TRANS@1>

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (BinNums.Z0 = BinNums.Z0)

  
  A : Type
  B : Type
  P : nat → A → B → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : P #|l| x y
  X : All2i_len P l l'
  IHX : BinInt.Z.of_nat #|l| = BinInt.Z.of_nat #|l'|
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l'|)
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH) =
    BinInt.Z.add (BinInt.Z.of_nat #|l'|) (BinNums.Zpos BinNums.xH))


DEBUG:Going to execute:
xlia zchecker

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (BinNums.Z0 = BinNums.Z0)

  
  A : Type
  B : Type
  P : nat → A → B → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : P #|l| x y
  X : All2i_len P l l'
  IHX : BinInt.Z.of_nat #|l| = BinInt.Z.of_nat #|l'|
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l'|)
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   (BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH) =
    BinInt.Z.add (BinInt.Z.of_nat #|l'|) (BinNums.Zpos BinNums.xH))


DEBUG:Going to execute:
<coq-core.plugins.micromega::Lia@0> $1