Goal:
  
  A : Type
  B : Type
  l : list A
  f : A -> option B
  g : A -> option B
  x : list B
  Hfg : forall (x : A) (y : B), f x = Some y -> g x = Some y
  ============================
   (map_option_out (map f l) = Some x -> map_option_out (map g l) = Some x)


DEBUG:Going to execute:
induction l in x |- *; simpl