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


DEBUG:Going to execute:
induction 2

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

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


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