let rec add a b (el, sl) =
  assert(not(is_interp a));
  if Term.eq a b then 
    (el, sl)
  else if inconsistent a b then
    raise Exc.Inconsistent
  else 
    match is_fresh_bv_var a, is_fresh_bv_var b with 
      | false, false ->
          (inste el a b, (a,b) :: insts sl a b)
      | true, true -> 
          (inste el a b, insts sl a b)
      | true, false -> 
          if is_interp b then
            (inste el a b, insts sl a b)
          else
            (inste el b a, insts sl b a)
      | false, true ->
          (inste el b a, insts sl b a) 

and is_fresh_bv_var _ = false    
     
and inste el a b = 
  List.map (fun (x,y) -> (apply1 x a b, apply1 y a b)) el

and insts sl a b =
  List.map (fun (x,y) -> (x, apply1 y a b)) sl 
  
and inconsistent a b =
  match width a, width b with
    | Some(n), Some(m) -> n <> m
    | _ -> false

and apply1 a x b =      (* substitute [x] by [b] in [a]. *)
  map (fun y -> if Term.eq x y then b else y) a