Goal:
    A : Type  P : A → Type  l : list A  x : A
  ============================
   (In x l → All P l → ∥ P x ∥)


DEBUG:Going to execute:
induction 2

Goals:
    A : Type  P : A → Type  x : A  H : In x []
  ============================
   (∥ P x ∥)

  
  A : Type
  P : A → Type
  x : A
  x0 : A
  l : list A
  H : In x (x0 :: l)
  p : P x0
  X : All P l
  IHX : In x l → ∥ P x ∥
  ============================
   (∥ P x ∥)


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