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' |- *

Goals:
    A : Type  P : A → Prop  l' : list A
  ============================
   (map_option_out [] = Some l' → All P l')

  
  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'
  ============================
   (map_option_out (x :: l) = Some l' → All P l')


DEBUG:Going to execute:
cbn

Goals:
    A : Type  P : A → Prop  l' : list A
  ============================
   (Some [] = Some l' → All P l')

  
  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'
  ============================
   (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:
inversion 1

Goals:
    A : Type  P : A → Prop  l' : list A  H : Some [] = Some l'  H1 : [] = l'
  ============================
   (All P [])

  
  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:
subst

Goals:
    A : Type  P : A → Prop  l' : list A  H : Some [] = Some l'  H1 : [] = l'
  ============================
   (All P [])

  
  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:
<coq-core.plugins.ltac::subst@1>

Goals:
    A : Type  P : A → Prop  H : Some [] = Some []
  ============================
   (All P [])

  
  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:
try constructor