Goal:
  
  A : Type
  P : A → Prop
  a : A
  l : list (option A)
  p : on_Some_or_None P (Some a)
  X : All (on_Some_or_None P) l
  IHX : ∀ l' : list A, map_option_out l = Some l' → All P l'
  l0 : list A
  H : match map_option_out l with
      | Some tl => Some (a :: tl)
      | None => None
      end = Some (a :: l0)
  e : map_option_out l = Some l0
  H1 : Some (a :: l0) = Some (a :: l0)
  ============================
   (All P (a :: l0))


DEBUG:Going to execute:
constructor