Goal:
  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  node_empty : node Empty None Empty = empty
  ============================
   (forall (l : tree A) (o : option A) (r : tree A),
    tree_case (Node l o r) = node l o r)


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

Goals:
  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  node_empty : node Empty None Empty = empty
  a : A
  ============================
   (tree_case (Node Empty (Some a) Empty) = node Empty (Some a) Empty)

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

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

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

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

  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  node_empty : node Empty None Empty = empty
  t0 : tree' A
  a : A
  t1 : tree' A
  ============================
   (tree_case (Node (Nodes t0) (Some a) (Nodes t1)) =
    node (Nodes t0) (Some a) (Nodes t1))

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

  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  node_empty : node Empty None Empty = empty
  t0 : tree' A
  t1 : tree' A
  ============================
   (tree_case (Node (Nodes t0) None (Nodes t1)) =
    node (Nodes t0) None (Nodes t1))


DEBUG:Going to execute:
simpl

Goals:
  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  node_empty : node Empty None Empty = empty
  a : A
  ============================
   (tree_case (Node Empty (Some a) Empty) = node Empty (Some a) Empty)

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

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

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

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

  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  node_empty : node Empty None Empty = empty
  t0 : tree' A
  a : A
  t1 : tree' A
  ============================
   (tree_case (Node (Nodes t0) (Some a) (Nodes t1)) =
    node (Nodes t0) (Some a) (Nodes t1))

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

  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  node_empty : node Empty None Empty = empty
  t0 : tree' A
  t1 : tree' A
  ============================
   (tree_case (Node (Nodes t0) None (Nodes t1)) =
    node (Nodes t0) None (Nodes t1))


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  node_empty : node Empty None Empty = empty
  a : A
  ============================
   (tree_case (Node Empty (Some a) Empty) = node Empty (Some a) Empty)

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

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

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

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

  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  node_empty : node Empty None Empty = empty
  t0 : tree' A
  a : A
  t1 : tree' A
  ============================
   (tree_case (Node (Nodes t0) (Some a) (Nodes t1)) =
    node (Nodes t0) (Some a) (Nodes t1))

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

  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  node_empty : node Empty None Empty = empty
  t0 : tree' A
  t1 : tree' A
  ============================
   (tree_case (Node (Nodes t0) None (Nodes t1)) =
    node (Nodes t0) None (Nodes t1))


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