Goal:
    A : Type  B : Type  empty : B  node : tree A -> option A -> tree A -> B
  ============================
   (forall (l : tree A) (o : option A) (r : tree A),
    not_trivially_empty l o r -> 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
  a : A
  ============================
   (not_trivially_empty Empty (Some a) Empty ->
    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
  a : A
  t0 : tree' A
  ============================
   (not_trivially_empty Empty (Some a) (Nodes t0) ->
    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
  ============================
   (not_trivially_empty Empty None 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
  t0 : tree' A
  ============================
   (not_trivially_empty Empty None (Nodes t0) ->
    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
  t0 : tree' A
  a : A
  ============================
   (not_trivially_empty (Nodes t0) (Some a) Empty ->
    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
  t0 : tree' A
  a : A
  t1 : tree' A
  ============================
   (not_trivially_empty (Nodes t0) (Some a) (Nodes t1) ->
    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
  t0 : tree' A
  ============================
   (not_trivially_empty (Nodes t0) None Empty ->
    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
  t0 : tree' A
  t1 : tree' A
  ============================
   (not_trivially_empty (Nodes t0) None (Nodes t1) ->
    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
  a : A
  ============================
   (True -> 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
  a : A
  t0 : tree' A
  ============================
   (True ->
    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
  ============================
   (False -> tree_case (Node Empty None Empty) = node Empty None Empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  t0 : tree' A
  ============================
   (True ->
    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
  t0 : tree' A
  a : A
  ============================
   (True ->
    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
  t0 : tree' A
  a : A
  t1 : tree' A
  ============================
   (True ->
    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
  t0 : tree' A
  ============================
   (True ->
    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
  t0 : tree' A
  t1 : tree' A
  ============================
   (True ->
    tree_case (Node (Nodes t0) None (Nodes t1)) =
    node (Nodes t0) None (Nodes t1))


DEBUG:Going to execute:
intros

Goals:
  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  a : A
  H : True
  ============================
   (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
  a : A
  t0 : tree' A
  H : True
  ============================
   (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
  H : False
  ============================
   (tree_case (Node Empty None Empty) = node Empty None Empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  t0 : tree' A
  H : True
  ============================
   (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
  t0 : tree' A
  a : A
  H : True
  ============================
   (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
  t0 : tree' A
  a : A
  t1 : tree' A
  H : True
  ============================
   (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
  t0 : tree' A
  H : True
  ============================
   (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
  t0 : tree' A
  t1 : tree' A
  H : True
  ============================
   (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
  a : A
  H : True
  ============================
   (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
  a : A
  t0 : tree' A
  H : True
  ============================
   (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
  H : False
  ============================
   (tree_case (Node Empty None Empty) = node Empty None Empty)

  
  A : Type
  B : Type
  empty : B
  node : tree A -> option A -> tree A -> B
  t0 : tree' A
  H : True
  ============================
   (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
  t0 : tree' A
  a : A
  H : True
  ============================
   (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
  t0 : tree' A
  a : A
  t1 : tree' A
  H : True
  ============================
   (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
  t0 : tree' A
  H : True
  ============================
   (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
  t0 : tree' A
  t1 : tree' A
  H : True
  ============================
   (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