[
  "\b�u��:W��|��q=�v",
  [
    [
      "Vale.Lib.Meta.generic_injective_proof",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0",
        "unit_inversion", "unit_typing"
      ],
      0,
      "3c6e0af58a4fa1295f9d8604a41bf4ac"
    ],
    [
      "Vale.Lib.Meta.exists_elim2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_Exists",
        "equation_Prims.squash",
        "l_quant_interp_db797c8159c2ff0e452e5710032e8990",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_44642e3a180510ae019bc79a1726fc14"
      ],
      0,
      "90dce761c13d2558de122f0da330ead0"
    ]
  ]
]