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; simpl
DEBUG LTAC Evaluated term: foroptb
DEBUG LTAC Evaluated term: foroptb