[
  "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,
      "046bbb5320f47e8dcb826457519a9be1"
    ],
    [
      "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,
      "57e770f8035f5efc07789701a00a16c0"
    ],
    [
      "Vale.Interop.Types.down_view",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt16",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt32",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
        "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",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt16@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt32@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
        "equation_Vale.Interop.Types.base_typ_as_type",
        "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ"
      ],
      0,
      "3b506c4db173f81a912dab75d3e864f5"
    ],
    [
      "Vale.Interop.Types.b8_preorder",
      1,
      1,
      0,
      [ "@MaxIFuel_assumption", "@query", "bool_inversion" ],
      0,
      "c2aa7d732c4b7dff081555a3aabb80a2"
    ],
    [
      "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,
      "d36c9f0b0b534a721d5ff8c979a5b364"
    ]
  ]
]