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
  x1 : A
  l2 : tree' B
  x2 : B
  ============================
   (tree C)


DEBUG:Going to execute:
exact (combine'_r r2)
Level 0: Backtrace:

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

The variable r1 was not found in the current environment.