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


DEBUG:Going to execute:
destruct x
Level 0: Backtrace:

In environment
A : Type
P : A → Prop
l' : list A
x : option A
l : list (option A)
p : on_Some_or_None P x
X : All (on_Some_or_None P) l
IHX : ∀ l' : list A, map_option_out l = Some l' → All P l'
H,
H1 : match x with
     | Some hd =>
         match map_option_out l with
         | Some tl => Some (hd :: tl)
         | None => None
         end
     | None => None
     end = Some l'
Unable to unify "All ?M2759 (?M2760 :: ?M2761)" with 
"All P l'".
Level 0: Backtrace:

In environment
A : Type
P : A → Prop
l' : list A
x : option A
l : list (option A)
p : on_Some_or_None P x
X : All (on_Some_or_None P) l
IHX : ∀ l' : list A, map_option_out l = Some l' → All P l'
H,
H1 : match x with
     | Some hd =>
         match map_option_out l with
         | Some tl => Some (hd :: tl)
         | None => None
         end
     | None => None
     end = Some l'
Unable to unify "All ?M2759 (?M2760 :: ?M2761)" with 
"All P l'".