Goal:
    A : Type  Aeq : ReflectEq A  x : option A  y : option A
  ============================
   (reflect (option_extends x y) (option_extendsb x y))


DEBUG:Going to execute:
destruct x as [x| ], y as [y| ]
DEBUG LTAC Evaluated term: Hf

Goals:
    A : Type  Aeq : ReflectEq A  x : A  y : A
  ============================
   (reflect (option_extends (Some x) (Some y))
      (option_extendsb (Some x) (Some y)))

    A : Type  Aeq : ReflectEq A  x : A
  ============================
   (reflect (option_extends (Some x) None) (option_extendsb (Some x) None))

    A : Type  Aeq : ReflectEq A  y : A
  ============================
   (reflect (option_extends None (Some y)) (option_extendsb None (Some y)))

    A : Type  Aeq : ReflectEq A
  ============================
   (reflect (option_extends None None) (option_extendsb None None))


DEBUG:Going to execute:
cbn
DEBUG LTAC Evaluated term: x
DEBUG LTAC Evaluated term: y
DEBUG LTAC Evaluated term: y