Goal:
    A : Type  B : Type  C : Type  f : A -> B  g : B -> C  x : option A
  ============================
   (option_map g (option_map f x) = option_map (fun x : A => g (f x)) x)


DEBUG:Going to execute:
destruct x

Goals:
    A : Type  B : Type  C : Type  f : A -> B  g : B -> C  a : A
  ============================
   (option_map g (option_map f (Some a)) =
    option_map (fun x : A => g (f x)) (Some a))

    A : Type  B : Type  C : Type  f : A -> B  g : B -> C
  ============================
   (option_map g (option_map f None) = option_map (fun x : A => g (f x)) None)


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

Goals:
    A : Type  B : Type  C : Type  f : A -> B  g : B -> C  a : A
  ============================
   (option_map g (option_map f (Some a)) =
    option_map (fun x : A => g (f x)) (Some a))

    A : Type  B : Type  C : Type  f : A -> B  g : B -> C
  ============================
   (option_map g (option_map f None) = option_map (fun x : A => g (f x)) None)


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