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
  r2 : tree' B
  ============================
   (tree C)


DEBUG:Going to execute:
solve
[ exact
(combine'_by_tac l1 l2)
| exact
(combine'_l l1)
| exact
(combine'_r l2)
| exact
Empty ]
DEBUG LTAC Evaluated term: Node