anchor.diff:               (Const.string_of_int_lid, 1, unary_op arg_as_int string_of_int);
                (Const.string_of_bool_lid, 1, unary_op arg_as_bool string_of_bool);
                (Const.string_compare, 2, binary_op arg_as_string string_compare');
  +             (Const.op_Eq,          3, decidable_eq false);
  +             (Const.op_notEq,       3, decidable_eq true);
                (Const.p2l ["FStar"; "String"; "list_of_string"],
                                       1, unary_op arg_as_string list_of_string');
                (Const.p2l ["FStar"; "String"; "string_of_list"],
  
positive.code:         | _ ->
              failwith "Unexpected number of arguments"
      in
      let decidable_equality =
          [{name = Const.op_Eq;
           arity = 3;
           strong_reduction_ok=true;
           interpretation=interp_bool false};
           {name = Const.op_notEq;
           arity = 3;
           strong_reduction_ok=true;
           interpretation=interp_bool true}]
      in
      let propositional_equality =
          {name = Const.eq2_lid;
           arity = 3;
  
negative.code:     List.map as_primitive_step (basic_ops@bounded_arith_ops)
  
  let equality_ops : list<primitive_step> =
      let interp_prop (r:Range.range) (args:args) : option<term> =
          match args with
          | [(_typ, _); (a1, _); (a2, _)]    //eq2
  