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


DEBUG:Going to execute:
exact (f None (Some x2))
Level 0: Backtrace:

The variable x1 was not found in the current environment.
Level 0: Backtrace:

The variable x1 was not found in the current environment.