let apply (x, y) a =
    assert(Term.Equal.is_var (x, y));
    assert(is a);
    let subst z = if Term.eq x z then y else z in
      try
        (match d_interp a with
           | Sym.Create, [z] -> 
               let z' = subst z in
                 if z == z' then z else mk_create z'
           | Sym.Update, [z1; z2; z3] ->
               let z1' = subst z1 and z2' = subst z2 and z3' = subst z3 in
                 if z1 == z1' && z2 == z2' && z3 == z3' then a else mk_update z1' z2' z3'
           | Sym.Select, [z1; z2] ->
               let z1' = subst z1 and z2' = subst z2 in
                 if z1 == z1' && z2 == z2' then a else mk_select z1' z2'
           | _ -> 
               subst a)
      with
          Not_found -> subst a