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
  b : M.Raw.bst l
  pf : ~ M.Raw.bst r
  s := lt_tree_dec k l : {M.Raw.lt_tree k l} + {~ M.Raw.lt_tree k l}
  s0 := gt_tree_dec k r : {M.Raw.gt_tree k r} + {~ M.Raw.gt_tree k r}
  H : M.Raw.bst (M.Raw.Node l k n r z)
  x : T.t
  e : elt
  l0 : M.Raw.tree elt
  r0 : M.Raw.tree elt
  h : Int.Z_as_Int.t
  H4 : M.Raw.bst l
  H6 : M.Raw.bst r
  H7 : M.Raw.lt_tree k l
  H8 : M.Raw.gt_tree k r
  H0 : l0 = l
  H1 : x = k
  H2 : e = n
  H3 : r0 = r
  H5 : h = z
  ============================
   False


DEBUG:Going to execute:
<coq-core.plugins.ltac::subst@1>