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


DEBUG:Going to execute:
destruct m1 as [r1| x1| x1 r1| l1| l1 r1| l1 x1| l1 x1 r1];
            destruct m2 as [r2| x2| x2 r2| l2| l2 r2| l2 x2| l2 x2 r2]