Goal:
  
  A : Type
  B : Type
  a : A
  l : list A
  P : B → Type
  x : B
  l0 : list B
  p : P x
  X : All P l0
  IHX : ∀ l : list A, #|l| = #|l0| → All2 (λ (_ : A) (b : B), P b) l l0
  H : BinInt.Z.add (BinInt.Z.of_nat #|l|) (BinNums.Zpos BinNums.xH) =
      BinInt.Z.add (BinInt.Z.of_nat #|l0|) (BinNums.Zpos BinNums.xH)
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l0|)
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat #|l|)
  ============================
   False


DEBUG:Going to execute:
zify_saturate