[
  "¡\u0007c\u0014C\u001dçì|\u0004½¿ŸA™x",
  [
    [
      "EverCrypt.Bytes.cipher_tag",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_EverCrypt.Bytes.bytes",
        "equation_EverCrypt.Bytes.lbytes", "equation_FStar.Bytes.lbytes",
        "haseqFStar.Bytes_Tm_refine_b0383769854f2b8d05d9f8fb03a8cbd4",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_FStar.Bytes.bytes"
      ],
      0,
      "1c2a037e3b8a9c495c67ba8c8328d783"
    ],
    [
      "EverCrypt.Bytes.maybe_plaintext",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_EverCrypt.Bytes.bytes",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_FStar.Bytes.bytes"
      ],
      0,
      "acf1ba08a2ee2756f6949037dfdd3d12"
    ],
    [
      "EverCrypt.Bytes.__proj__Correct__item___0",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_EverCrypt.Bytes.Correct",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_EverCrypt.Bytes_Tm_refine_8669a1bbf2da46d63a758499ccd47453"
      ],
      0,
      "02f5def3c91feee42ee2d746cd94c122"
    ]
  ]
]