Goal:
    A : Type  B : Type  P : A → B → Type  l : list A  l' : list B  x' : B
  ============================
   (In x' l' → All2 P l l' → ∥ ∑ x : A, P x x' ∥)


DEBUG:Going to execute:
induction 2

Goals:
    A : Type  B : Type  P : A → B → Type  x' : B  H : In x' []
  ============================
   (∥ ∑ x : A, P x x' ∥)

  
  A : Type
  B : Type
  P : A → B → Type
  x' : B
  y : B
  l' : list B
  H : In x' (y :: l')
  x : A
  l : list A
  r : P x y
  X : All2 P l l'
  IHX : In x' l' → ∥ ∑ x : A, P x x' ∥
  ============================
   (∥ ∑ x : A, P x x' ∥)


DEBUG:Going to execute:
simpl in H => //