Goal:
  
  A : Type
  B : Type
  a : A
  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
  b : B
  fa : f a = Some b
  l0 : list B
  ============================
   ((forall x : list B, Some l0 = Some x -> map_option_out (map g l) = Some x) ->
    Some (b :: l0) = Some x ->
    match map_option_out (map g l) with
    | Some tl => Some (b :: tl)
    | None => None
    end = Some x)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrmove@1> $1 $2
DEBUG LTAC Evaluated term: map_option_out