[
  "x�o��\u0016쀮���\n�Us",
  [
    [
      "Vale.Interop.Types.base_typ_as_type",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_FStar.UInt16.t__uu___haseq",
        "assumption_FStar.UInt32.t__uu___haseq",
        "assumption_FStar.UInt64.t__uu___haseq",
        "assumption_FStar.UInt8.t__uu___haseq",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt128",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt16",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt32",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt64",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt8",
        "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ"
      ],
      0,
      "f5ae00132d34ca2283c014b8f0b63cf7"
    ],
    [
      "Vale.Interop.Types.view_n_unfold",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt128",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt16",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt32",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt64",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt8",
        "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ"
      ],
      0,
      "dcd43df24578816e7d8b94e2196b7fa8"
    ],
    [
      "Vale.Interop.Types.down_view",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt128",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt16",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt32",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt64",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt8",
        "equation_Vale.Interop.Types.base_typ_as_type",
        "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "1498f408605d07639dea86ebbab0eaac"
    ],
    [
      "Vale.Interop.Types.b8_preorder",
      1,
      1,
      0,
      [ "@MaxIFuel_assumption", "@query", "bool_inversion" ],
      0,
      "b2e8f57a3d5934867b8747b50f748ae3"
    ],
    [
      "Vale.Interop.Types.__proj__Buffer__item__bsrc",
      1,
      1,
      0,
      [
        "@query", "proj_equation_Vale.Interop.Types.Buffer_src",
        "proj_equation_Vale.Interop.Types.Buffer_writeable",
        "projection_inverse_Vale.Interop.Types.Buffer_src",
        "projection_inverse_Vale.Interop.Types.Buffer_writeable"
      ],
      0,
      "e1fbe574ea3a1adb030a50d0ac5b0519"
    ],
    [
      "Vale.Interop.Types.base_typ_as_type",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_FStar.UInt16.t__uu___haseq",
        "assumption_FStar.UInt32.t__uu___haseq",
        "assumption_FStar.UInt64.t__uu___haseq",
        "assumption_FStar.UInt8.t__uu___haseq",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt128",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt16",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt32",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt64",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt8",
        "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ"
      ],
      0,
      "e570f7957dfb4787535db9793ee753cd"
    ],
    [
      "Vale.Interop.Types.view_n_unfold",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt128",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt16",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt32",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt64",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt8",
        "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ"
      ],
      0,
      "28d8a60387693e566140eacff8ebf85e"
    ],
    [
      "Vale.Interop.Types.down_view",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt128",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt16",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt32",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt64",
        "disc_equation_Vale.Arch.HeapTypes_s.TUInt8",
        "equation_Vale.Interop.Types.base_typ_as_type",
        "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "f76342ae074080e444ba2d3fee0e1164"
    ],
    [
      "Vale.Interop.Types.b8_preorder",
      2,
      1,
      0,
      [ "@MaxIFuel_assumption", "@query", "bool_inversion" ],
      0,
      "34bc1d013f718002331e8b93bc0e84ff"
    ],
    [
      "Vale.Interop.Types.__proj__Buffer__item__bsrc",
      2,
      1,
      0,
      [
        "@query", "proj_equation_Vale.Interop.Types.Buffer_src",
        "proj_equation_Vale.Interop.Types.Buffer_writeable",
        "projection_inverse_Vale.Interop.Types.Buffer_src",
        "projection_inverse_Vale.Interop.Types.Buffer_writeable"
      ],
      0,
      "365ac990d3d916d86f5741970ae3dc45"
    ]
  ]
]