Goal:
  
  elt : Type
  bst_dec : forall t : M.Raw.tree elt, {M.Raw.bst t} + {~ M.Raw.bst t}
  t : M.Raw.tree elt
  l : M.Raw.tree elt
  k : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : M.Raw.bst l
  p2 : M.Raw.bst r
  p3 : M.Raw.lt_tree k l
  p4 : M.Raw.gt_tree k r
  ============================
   (M.Raw.bst (M.Raw.Node l k n r z))


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>

Goals:
  
  elt : Type
  bst_dec : forall t : M.Raw.tree elt, {M.Raw.bst t} + {~ M.Raw.bst t}
  t : M.Raw.tree elt
  l : M.Raw.tree elt
  k : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : M.Raw.bst l
  p2 : M.Raw.bst r
  p3 : M.Raw.lt_tree k l
  p4 : M.Raw.gt_tree k r
  ============================
   (M.Raw.bst l)

  
  elt : Type
  bst_dec : forall t : M.Raw.tree elt, {M.Raw.bst t} + {~ M.Raw.bst t}
  t : M.Raw.tree elt
  l : M.Raw.tree elt
  k : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : M.Raw.bst l
  p2 : M.Raw.bst r
  p3 : M.Raw.lt_tree k l
  p4 : M.Raw.gt_tree k r
  ============================
   (M.Raw.bst r)

  
  elt : Type
  bst_dec : forall t : M.Raw.tree elt, {M.Raw.bst t} + {~ M.Raw.bst t}
  t : M.Raw.tree elt
  l : M.Raw.tree elt
  k : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : M.Raw.bst l
  p2 : M.Raw.bst r
  p3 : M.Raw.lt_tree k l
  p4 : M.Raw.gt_tree k r
  ============================
   (M.Raw.lt_tree k l)

  
  elt : Type
  bst_dec : forall t : M.Raw.tree elt, {M.Raw.bst t} + {~ M.Raw.bst t}
  t : M.Raw.tree elt
  l : M.Raw.tree elt
  k : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : M.Raw.bst l
  p2 : M.Raw.bst r
  p3 : M.Raw.lt_tree k l
  p4 : M.Raw.gt_tree k r
  ============================
   (M.Raw.gt_tree k r)


DEBUG:Going to execute:
assumption

Goals:
  
  elt : Type
  bst_dec : forall t : M.Raw.tree elt, {M.Raw.bst t} + {~ M.Raw.bst t}
  t : M.Raw.tree elt
  l : M.Raw.tree elt
  k : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : M.Raw.bst l
  p2 : M.Raw.bst r
  p3 : M.Raw.lt_tree k l
  p4 : M.Raw.gt_tree k r
  ============================
   (M.Raw.bst l)

  
  elt : Type
  bst_dec : forall t : M.Raw.tree elt, {M.Raw.bst t} + {~ M.Raw.bst t}
  t : M.Raw.tree elt
  l : M.Raw.tree elt
  k : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : M.Raw.bst l
  p2 : M.Raw.bst r
  p3 : M.Raw.lt_tree k l
  p4 : M.Raw.gt_tree k r
  ============================
   (M.Raw.bst r)

  
  elt : Type
  bst_dec : forall t : M.Raw.tree elt, {M.Raw.bst t} + {~ M.Raw.bst t}
  t : M.Raw.tree elt
  l : M.Raw.tree elt
  k : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : M.Raw.bst l
  p2 : M.Raw.bst r
  p3 : M.Raw.lt_tree k l
  p4 : M.Raw.gt_tree k r
  ============================
   (M.Raw.lt_tree k l)

  
  elt : Type
  bst_dec : forall t : M.Raw.tree elt, {M.Raw.bst t} + {~ M.Raw.bst t}
  t : M.Raw.tree elt
  l : M.Raw.tree elt
  k : M.Raw.key
  n : elt
  r : M.Raw.tree elt
  z : Int.Z_as_Int.t
  p1 : M.Raw.bst l
  p2 : M.Raw.bst r
  p3 : M.Raw.lt_tree k l
  p4 : M.Raw.gt_tree k r
  ============================
   (M.Raw.gt_tree k r)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::assumption@0>