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]

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

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

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

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

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

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

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


DEBUG:Going to execute:
destruct m2 as [r2| x2| x2 r2| l2| l2 r2| l2 x2| l2 x2 r2]
DEBUG LTAC Evaluated term: m1

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

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

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

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

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

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

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

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

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

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

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

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

  
  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)

  
  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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


DEBUG:Going to execute:
apply Node;
            [ solve
            [ exact
            (combine'_by_tac l1 l2)
            | exact
            (combine'_l l1)
            | exact
            (combine'_r l2)
            | exact
            Empty ]
            | solve
            [ exact
            (f (Some x1) (Some x2))
            | exact
            (f None (Some x2))
            | exact
            (f (Some x1) None)
            | exact
            None ]
            | solve
            [ exact
            (combine'_by_tac r1 r2)
            | exact
            (combine'_l r1)
            | exact
            (combine'_r r2)
            | exact
            Empty ] ]
DEBUG LTAC Evaluated term: m2
DEBUG LTAC Evaluated term: m2
DEBUG LTAC Evaluated term: m2
DEBUG LTAC Evaluated term: m2
DEBUG LTAC Evaluated term: m2
DEBUG LTAC Evaluated term: m2
DEBUG LTAC Evaluated term: m2