V.restrict

let restrict x s =

  try

    let (y, prf) = apply s x in              (* [prf |- x = y]. *)

      Trace.msg "v" "Restrict" x Term.pp;

      let  (y, _) = find s y in              (* now get canonical [y]. *)

      let find' =

        let newfind = Map.remove x s.find in (* remove [x |-> y]. *)

          try

            let invx = inv s x in            (* for all [z |-> x], set [z |-> y]. *)

              Set.fold

                (fun z -> Map.add z (y, None))

                invx

                newfind

          with

              Not_found -> newfind

      in

      let inv' =

        let newinv = Map.remove x s.inv in

(** remove the inverse of x. *)



          try 

            let invy = inv s y in           (* remove [x] from the inverse of [y]. *)

            let invy' = Set.remove x invy in

              if Set.is_empty invy' then 

                Map.remove y newinv

              else 

                Map.add y invy' newinv

          with

              Not_found -> newinv

      in

        {find = find'; inv = inv'; removable = Set.remove x s.removable}

  with

      Not_found -> s