Goal:
    A : Type  B : Type  P : nat → A → B → Type  l : list A  l' : list B
  ============================
   (All2i_len P l l' → #|l| = #|l'|)


DEBUG:Going to execute:
induction 1

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (#|[]| = #|[]|)

  
  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 : #|l| = #|l'|
  ============================
   (#|x :: l| = #|y :: l'|)


DEBUG:Going to execute:
simpl

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
lia

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
Zify.zify; xlia zchecker

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
Zify.zify

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations;
            Zify.zify_post_hook; zify_saturate

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations;
            Zify.zify_post_hook

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
intros

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
Zify.zify_pre_hook

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
idtac

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
zify_elim_let

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


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

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


DEBUG:Going to execute:
zify_op

Goals:
    A : Type  B : Type  P : nat → A → B → Type
  ============================
   (0 = 0)

  
  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 : #|l| = #|l'|
  ============================
   (S #|l| = S #|l'|)


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

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_iter_specs

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:
fun => <coq-core.plugins.zify::ITER@0>

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_to_euclidean_division_equations

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:
lazymatch Zify.zify_convert_to_euclidean_division_equations_flag
           with
           | true =>
               Zify.zify_internal_to_euclidean_division_equations
           | false => idtac
           end

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_convert_to_euclidean_division_equations_flag

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:
constr:(false)