Goal:
  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  ============================
   (forall (l : tree A) (o : option A) (r : tree A),
    not_trivially_empty l o r ->
    tree_rec (Node l o r) = node l (tree_rec l) o r (tree_rec r))


DEBUG:Going to execute:
destruct l, o, r

Goals:
  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  a : A
  ============================
   (not_trivially_empty Empty (Some a) Empty ->
    tree_rec (Node Empty (Some a) Empty) =
    node Empty (tree_rec Empty) (Some a) Empty (tree_rec Empty))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  a : A
  t0 : tree' A
  ============================
   (not_trivially_empty Empty (Some a) (Nodes t0) ->
    tree_rec (Node Empty (Some a) (Nodes t0)) =
    node Empty (tree_rec Empty) (Some a) (Nodes t0) (tree_rec (Nodes t0)))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  ============================
   (not_trivially_empty Empty None Empty ->
    tree_rec (Node Empty None Empty) =
    node Empty (tree_rec Empty) None Empty (tree_rec Empty))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  ============================
   (not_trivially_empty Empty None (Nodes t0) ->
    tree_rec (Node Empty None (Nodes t0)) =
    node Empty (tree_rec Empty) None (Nodes t0) (tree_rec (Nodes t0)))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  a : A
  ============================
   (not_trivially_empty (Nodes t0) (Some a) Empty ->
    tree_rec (Node (Nodes t0) (Some a) Empty) =
    node (Nodes t0) (tree_rec (Nodes t0)) (Some a) Empty (tree_rec Empty))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  a : A
  t1 : tree' A
  ============================
   (not_trivially_empty (Nodes t0) (Some a) (Nodes t1) ->
    tree_rec (Node (Nodes t0) (Some a) (Nodes t1)) =
    node (Nodes t0) (tree_rec (Nodes t0)) (Some a) 
      (Nodes t1) (tree_rec (Nodes t1)))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  ============================
   (not_trivially_empty (Nodes t0) None Empty ->
    tree_rec (Node (Nodes t0) None Empty) =
    node (Nodes t0) (tree_rec (Nodes t0)) None Empty (tree_rec Empty))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  t1 : tree' A
  ============================
   (not_trivially_empty (Nodes t0) None (Nodes t1) ->
    tree_rec (Node (Nodes t0) None (Nodes t1)) =
    node (Nodes t0) (tree_rec (Nodes t0)) None (Nodes t1)
      (tree_rec (Nodes t1)))


DEBUG:Going to execute:
simpl

Goals:
  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  a : A
  ============================
   (True ->
    tree_rec (Node Empty (Some a) Empty) =
    node Empty empty (Some a) Empty empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  a : A
  t0 : tree' A
  ============================
   (True ->
    tree_rec (Node Empty (Some a) (Nodes t0)) =
    node Empty empty (Some a) (Nodes t0) (tree_rec' t0))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  ============================
   (False ->
    tree_rec (Node Empty None Empty) = node Empty empty None Empty empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  ============================
   (True ->
    tree_rec (Node Empty None (Nodes t0)) =
    node Empty empty None (Nodes t0) (tree_rec' t0))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  a : A
  ============================
   (True ->
    tree_rec (Node (Nodes t0) (Some a) Empty) =
    node (Nodes t0) (tree_rec' t0) (Some a) Empty empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  a : A
  t1 : tree' A
  ============================
   (True ->
    tree_rec (Node (Nodes t0) (Some a) (Nodes t1)) =
    node (Nodes t0) (tree_rec' t0) (Some a) (Nodes t1) (tree_rec' t1))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  ============================
   (True ->
    tree_rec (Node (Nodes t0) None Empty) =
    node (Nodes t0) (tree_rec' t0) None Empty empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  t1 : tree' A
  ============================
   (True ->
    tree_rec (Node (Nodes t0) None (Nodes t1)) =
    node (Nodes t0) (tree_rec' t0) None (Nodes t1) (tree_rec' t1))


DEBUG:Going to execute:
intros

Goals:
  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  a : A
  H : True
  ============================
   (tree_rec (Node Empty (Some a) Empty) =
    node Empty empty (Some a) Empty empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  a : A
  t0 : tree' A
  H : True
  ============================
   (tree_rec (Node Empty (Some a) (Nodes t0)) =
    node Empty empty (Some a) (Nodes t0) (tree_rec' t0))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  H : False
  ============================
   (tree_rec (Node Empty None Empty) = node Empty empty None Empty empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  H : True
  ============================
   (tree_rec (Node Empty None (Nodes t0)) =
    node Empty empty None (Nodes t0) (tree_rec' t0))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  a : A
  H : True
  ============================
   (tree_rec (Node (Nodes t0) (Some a) Empty) =
    node (Nodes t0) (tree_rec' t0) (Some a) Empty empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  a : A
  t1 : tree' A
  H : True
  ============================
   (tree_rec (Node (Nodes t0) (Some a) (Nodes t1)) =
    node (Nodes t0) (tree_rec' t0) (Some a) (Nodes t1) (tree_rec' t1))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  H : True
  ============================
   (tree_rec (Node (Nodes t0) None Empty) =
    node (Nodes t0) (tree_rec' t0) None Empty empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  t1 : tree' A
  H : True
  ============================
   (tree_rec (Node (Nodes t0) None (Nodes t1)) =
    node (Nodes t0) (tree_rec' t0) None (Nodes t1) (tree_rec' t1))


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  a : A
  H : True
  ============================
   (tree_rec (Node Empty (Some a) Empty) =
    node Empty empty (Some a) Empty empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  a : A
  t0 : tree' A
  H : True
  ============================
   (tree_rec (Node Empty (Some a) (Nodes t0)) =
    node Empty empty (Some a) (Nodes t0) (tree_rec' t0))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  H : False
  ============================
   (tree_rec (Node Empty None Empty) = node Empty empty None Empty empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  H : True
  ============================
   (tree_rec (Node Empty None (Nodes t0)) =
    node Empty empty None (Nodes t0) (tree_rec' t0))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  a : A
  H : True
  ============================
   (tree_rec (Node (Nodes t0) (Some a) Empty) =
    node (Nodes t0) (tree_rec' t0) (Some a) Empty empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  a : A
  t1 : tree' A
  H : True
  ============================
   (tree_rec (Node (Nodes t0) (Some a) (Nodes t1)) =
    node (Nodes t0) (tree_rec' t0) (Some a) (Nodes t1) (tree_rec' t1))

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  H : True
  ============================
   (tree_rec (Node (Nodes t0) None Empty) =
    node (Nodes t0) (tree_rec' t0) None Empty empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> B -> option A -> tree A -> B -> B
  t0 : tree' A
  t1 : tree' A
  H : True
  ============================
   (tree_rec (Node (Nodes t0) None (Nodes t1)) =
    node (Nodes t0) (tree_rec' t0) None (Nodes t1) (tree_rec' t1))


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3