Goal:
  
  A : Type
  B : Type
  C : Type
  f : option A -> option B -> option C
  f_None_None : f None None = None
  ============================
   (combine'_by_tac = combine'_direct)


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