Insertion in sorted tree

module Bintree_insert

  use import bintree.Tree
  use import bintree.Size
  use import bintree.Inorder
  use import bintree.InorderLength
  use import int.Int
(*-------------------------------*)

  function num_occ (x: 'a) (l: tree 'a) : int =
    match l with
    | Empty -> 0
    | Node t1 y t2 -> (if x = y then 1 else 0) + num_occ x t1 + num_occ x t2
   end

(*-------------------------------*)

  let rec add (t : tree int) (v : int) : tree int =
    ensures {forall x : int. num_occ x result =
             if x = v then 1 + num_occ x t else num_occ x t }
    match t with
     | Empty -> Node (Empty) v (Empty)
     | Node t1 x t2 ->
       if v <= x then Node (add t1 v) x t2 else Node t1 x (add t2 v)
    end

end