anchor.diff:    | (TApp (x, ys), TApp (u, vs)) -> 
       let tc = List.fold2 (fun (l:typ_constraints) t1 t2 -> l@[(t1, t2)]) [] ys vs in
       unify env m ([(x, u)]@tc)
  +  | (TName (Id "bool"), TName (Id "prop")) 
  +  | (TName (Id "prop"), TName (Id "bool")) -> 
  +    let u = TName (Id "prop") in
  +    let m = bind_typ m s u in bind_typ m t u
     | (TName (Id x), TName (Id y)) -> 
       if x = y then m else err ("type mismatch ")
     | _ -> err ("type mismatch ")
  
positive.code:       let (t, ae, s) = infer_exp env e (Some et) in
        let ae = AEOp (Uop UOld, [ae], tv, et) in
        (tv, ae, s@[(t, tv)])
      | EOp (Bop op, [e1; e2]) when isArithmeticOp op ->
        // op in {+, -, *, /, %} 
        let tv = next_type_var() in
  
negative.code:       (tv, ae, s1@s2@[(t1, TName(Id "state"));(t2, tv)])
      | EOp (Bop (BCustom op), l) ->
        err ("missing typing rule for BCustom")
      | EOp (Subscript, [e1; e2]) ->
        let e = EApply ((Id "subscript"), [e1; e2]) in
        let (t, ae, s) = infer_exp env e expected_typ in
        let ae = 
          match ae with 
          | AEApply (x, es, [t], [et]) -> AEOp (Subscript, es, t, et)
          | _ -> err ("expect apply expression") in
        (t, ae, s)
      | EOp (Update, [e1; e2; e3]) -> 
        let e = EApply ((Id "update"), [e1; e2; e3]) in
        let (t, ae, s) = infer_exp env e expected_typ in
        let ae = 
          match ae with 
          | AEApply (x, es, [t], [et]) -> AEOp (Update, es, t, et)
          | _ -> err ("expect apply expression") in
        (t, ae, s)
      | EOp (Cond, [e1; e2; e3]) -> 
        let tv = next_type_var() in
        let et = match expected_typ with | None -> tv | Some t -> t in
        let (t1, ae1, s1) = infer_exp env e1 None in
        let (t2, ae2, s2) = infer_exp env e2 (Some et) in
        let (t3, ae3, s3) = infer_exp env e3 (Some et) in
        let ae = AEOp (Cond, [ae1; ae2; ae3], tv, et) in
        (tv, ae, s1@s2@s3@[(t1, TName(Id "bool")); (t2, tv);(t3, tv)])
      | EOp (FieldOp x, [e]) -> 
        let (t1, _, _) = infer_exp env e None in
        let (t, ae, s) = 
          match (t1,x) with 
          | (TName (Id t), (Id f)) ->
            let s = "__proj" + t + "__item__" + f in
            let e = EApply (Id s, [e]) in
            infer_exp env e expected_typ
          | _ -> err ("unknown field type") in
        let ae = 
          match ae with 
          | AEApply (x, es, [t], [et]) -> AEOp (FieldOp x, es, t, et)
          | _ -> err ("expect apply expression") in
        (t, ae, s)
      | EOp (FieldUpdate x, [e1; e2]) -> 
        let (t1, _, _) = infer_exp env e1 None in
        let (t2, ae2, s2) = infer_exp env e2 None in
        let (t, ae, s) = 
          match (t1,x) with 
          | (TName (Id t), (Id f)) ->
            let s = "__proj" + t + "__item__" + f in
            let e = EApply (Id s, [e1]) in
            infer_exp env e expected_typ
          | _ -> err ("not implemented field op") in
        let ae = 
          match ae with 
          | AEApply (x, es, [t], [et]) -> AEOp (FieldUpdate x, es@[ae2], t, et)
          | _ -> err ("expect apply expression") in
        (t, ae, s@s2@[(t2, t)])
      | EOp (op, es) -> 
        err ("unsupported Eop ") 
      | EApply (Id "list", es) ->
        let tv = next_type_var() in
        let arg_typ = next_type_var() in
  