anchor.diff:        let e = eapply (Operator (x + "[:=]")) [e1; e2; e3] in
         let (t, ae) = infer_exp env u e expected_typ in
         match ae with
  -      | (AE_Apply (_, _, es), _) -> ret t.norm_typ (AE_Op (Update, es)) // TODO: save x or t1
  +      | (AE_Apply (_, _, es), _) -> ret t (AE_Op (Update, es)) // TODO: save x or t1
         | _ -> internalErr ("EOp Update")
       )
     | EOp (Bop BIn, [e1; e2]) ->
  
positive.code:     let (t, ae) = infer_exp env u e et in
      //printfn "t = %A  ae = %A  u = %A" t ae u;
      u_unify u None;
      let t = subst_typ u.u_substs t.norm_typ in
      let es = subst_exp env u.u_substs ae in
  //    printfn "e = %A  es = %A" (Emit_vale_text.string_of_exp e) (Emit_vale_text.string_of_exp es);
  //    printfn "e = %A\n  ae = %A\n  t = %A\n  es = %A" e ae t es;
  
negative.code:   | None -> e
    | Some (t, et) -> if typ_equal env t et then e else insert_cast e t et
  
  let rec infer_arg_typ (env:env) (u:unifier) (args:(exp * typ option) list):(typ list * aexp list) =
    let infer_arg_typ_fold (ts, ae) ((e:exp), (et:typ option)):(typ list * aexp list) =
      let (t, ae1) =
  (*
        let tr =
  