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

Goals:
  
  A : Type
  B : Type
  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 []) = Some x -> map_option_out (map g []) = Some x)

  
  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
  IHl : forall x : list B,
        map_option_out (map f l) = Some x ->
        map_option_out (map g l) = Some x
  ============================
   (map_option_out (map f (a :: l)) = Some x ->
    map_option_out (map g (a :: l)) = Some x)


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: l

Goals:
  
  A : Type
  B : Type
  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
  ============================
   (Some [] = Some x -> Some [] = Some x)

  
  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
  IHl : forall x : list B,
        map_option_out (map f l) = Some x ->
        map_option_out (map g l) = Some x
  ============================
   (match f a with
    | Some hd =>
        match map_option_out (map f l) with
        | Some tl => Some (hd :: tl)
        | None => None
        end
    | None => None
    end = Some x ->
    match g a with
    | Some hd =>
        match map_option_out (map g l) with
        | Some tl => Some (hd :: tl)
        | None => None
        end
    | None => None
    end = Some x)


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  B : Type
  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
  ============================
   (Some [] = Some x -> Some [] = Some x)

  
  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
  IHl : forall x : list B,
        map_option_out (map f l) = Some x ->
        map_option_out (map g l) = Some x
  ============================
   (match f a with
    | Some hd =>
        match map_option_out (map f l) with
        | Some tl => Some (hd :: tl)
        | None => None
        end
    | None => None
    end = Some x ->
    match g a with
    | Some hd =>
        match map_option_out (map g l) with
        | Some tl => Some (hd :: tl)
        | None => None
        end
    | None => None
    end = Some x)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3