Goal:
  
  A : Type
  P : A → Prop
  l' : list A
  l : list (option A)
  p : on_Some_or_None P None
  X : All (on_Some_or_None P) l
  IHX : ∀ l' : list A, map_option_out l = Some l' → All P l'
  H : None = Some l'
  H1 : None = Some l'
  ============================
   (All P l')


DEBUG:Going to execute:
<coq-core.plugins.ltac::discriminate@0>