Goal:
    A : Type  f : A -> bool  g : A -> bool  Hfg : f =1 g  y : option A
  ============================
   (option_get true (option_map f y) = option_get true (option_map g y))


DEBUG:Going to execute:
destruct y

Goals:
    A : Type  f : A -> bool  g : A -> bool  Hfg : f =1 g  a : A
  ============================
   (option_get true (option_map f (Some a)) =
    option_get true (option_map g (Some a)))

    A : Type  f : A -> bool  g : A -> bool  Hfg : f =1 g
  ============================
   (option_get true (option_map f None) = option_get true (option_map g None))


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

Goals:
    A : Type  f : A -> bool  g : A -> bool  Hfg : f =1 g  a : A
  ============================
   (f a = g a)

    A : Type  f : A -> bool  g : A -> bool  Hfg : f =1 g
  ============================
   (true = true)


DEBUG:Going to execute:
rewrite // ?Hfg