[
  "\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,
      "9c70838c98ef975a4f5e6f1526255f81"
    ],
    [
      "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,
      "8604d221152791ca014ab80e3be7a5f2"
    ]
  ]
]