Goal:
    A : Type  P : A → Prop  l : list (option A)  l' : list A
  ============================
   (All (on_Some_or_None P) l → map_option_out l = Some l' → All P l')


DEBUG:Going to execute:
induction 1 in l' |- *; cbn; inversion 1