let is_cmp (#a:eqtype) (is_le:a -> a -> bool) =
  (forall (x y:a).{:pattern is_le x y} is_le x y \/ is_le y x) /\
  (forall (x y:a).{:pattern is_le x y} is_le x y /\ is_le y x ==> x == y) /\
  (forall (x y z:a).{:pattern is_le x y; is_le y z} is_le x y /\ is_le y z ==> is_le x z)
let is_cmp (#a: eqtype) (is_le: (a -> a -> bool)) =
(forall (x: a) (y: a). {:pattern is_le x y} is_le x y \/ is_le y x) /\
(forall (x: a) (y: a). {:pattern is_le x y} is_le x y /\ is_le y x ==> x == y) /\
(forall (x: a) (y: a) (z: a). {:pattern is_le x y; is_le y z} is_le x y /\ is_le y z ==> is_le x z)
Vale.Lib.MapTree.fsti.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Lib.MapTree.fsti
Prims.eqtype Prims.bool Prims.l_and Prims.l_Forall Prims.l_or Prims.b2t Prims.l_imp Prims.eq2 Prims.logical
module Vale.Lib.MapTree
open FStar.Mul

(** Balanced binary search tree *)
val is_cmp : is_le: (_: a -> _: a -> Prims.bool) -> Prims.logical
is_le: (_: a -> _: a -> Prims.bool) -> Prims.logical