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 r1 r2)
| exact
(combine'_l r1)
| exact
(combine'_r r2)
| exact
Empty ]