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
  ============================
   (option C)


DEBUG:Going to execute:
PTRDEBUGTACsolve
[ exact
(f (Some x1) (Some x2))
| exact
(f None (Some x2))
| exact
(f (Some x1) None)
| exact
None ]