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 : S #|l| = S #|l0|
  ============================
   False


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