[
  "@SÂ\u0018ÔÜzhS^ü<;÷\r\u0004",
  [
    [
      "Spec.Hash.Lemmas0.max_input_size_len",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_224",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "disc_equation_Spec.Hash.Definitions.MD5",
        "disc_equation_Spec.Hash.Definitions.SHA1",
        "disc_equation_Spec.Hash.Definitions.SHA2_224",
        "disc_equation_Spec.Hash.Definitions.SHA2_256",
        "disc_equation_Spec.Hash.Definitions.SHA2_384",
        "disc_equation_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Hash.Definitions.is_md",
        "equation_Spec.Hash.Definitions.len_length",
        "equation_Spec.Hash.Definitions.max_input_length",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_md",
        "typing_Spec.Hash.Definitions.len_length"
      ],
      0,
      "b836eeef5d5cc121d50bdf05f1579205"
    ]
  ]
]