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|
  ============================
   (All2 (λ (_ : A) (b : B), P b) (a :: l) (x :: l0))


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::exfalso@0>