Goal:
  
  A : Type
  a : option A
  l : list (option A)
  f : A -> A
  IHl : map_option_out (map (option_map f) l) = option_map (map f) None
  a0 : A
  fa : option_map f a = Some a0
  ============================
   (None = option_map (map f) match a with
                              | Some _ | _ => None
                              end)


DEBUG:Going to execute:
destruct a

Goals:
  
  A : Type
  a : A
  l : list (option A)
  f : A -> A
  IHl : map_option_out (map (option_map f) l) = option_map (map f) None
  a0 : A
  fa : option_map f (Some a) = Some a0
  ============================
   (None = option_map (map f) None)

  
  A : Type
  l : list (option A)
  f : A -> A
  IHl : map_option_out (map (option_map f) l) = option_map (map f) None
  a0 : A
  fa : option_map f None = Some a0
  ============================
   (None = option_map (map f) None)


DEBUG:Going to execute:
reflexivity
DEBUG LTAC Evaluated term: a

Goals:
  
  A : Type
  a : A
  l : list (option A)
  f : A -> A
  IHl : map_option_out (map (option_map f) l) = option_map (map f) None
  a0 : A
  fa : option_map f (Some a) = Some a0
  ============================
   (None = option_map (map f) None)

  
  A : Type
  l : list (option A)
  f : A -> A
  IHl : map_option_out (map (option_map f) l) = option_map (map f) None
  a0 : A
  fa : option_map f None = Some a0
  ============================
   (None = option_map (map f) None)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>