[
  "¯Šï\"OÍ€\\Ær}9\u0002?\u0003s",
  [
    [
      "Vale.Def.Words.Seq.two_to_seq_to_two_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words.Seq_s.seq2",
        "equation_Vale.Def.Words.Seq_s.seq_to_two_LE",
        "equation_Vale.Def.Words.Seq_s.seqn", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "proj_equation_Vale.Def.Words_s.Mktwo_hi",
        "proj_equation_Vale.Def.Words_s.Mktwo_lo",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mktwo_hi",
        "projection_inverse_Vale.Def.Words_s.Mktwo_lo",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f9ee523a22c7eb000c4c8d4de6592dcb",
        "typing_Vale.Def.Words.Seq_s.seq_to_two_LE",
        "typing_Vale.Def.Words.Seq_s.two_to_seq_LE"
      ],
      0,
      "479aadefb7ae6f0c646002ecab68de1c"
    ],
    [
      "Vale.Def.Words.Seq.seq_to_two_to_seq_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.Def.Words.Seq_s.seq_to_two_LE",
        "fuel_guarded_inversion_Vale.Def.Words_s.two",
        "proj_equation_Vale.Def.Words_s.Mktwo_hi",
        "proj_equation_Vale.Def.Words_s.Mktwo_lo",
        "refinement_interpretation_Tm_refine_f9ee523a22c7eb000c4c8d4de6592dcb",
        "typing_Vale.Def.Words.Seq_s.two_to_seq_LE"
      ],
      0,
      "b0e028fe72b1a9c7c0e09cc8da9e0f92"
    ],
    [
      "Vale.Def.Words.Seq.seq_to_seq_four_to_seq_LE",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "a6bb30c70c41ce45135836472614fb82"
    ],
    [
      "Vale.Def.Words.Seq.seq_to_seq_four_to_seq_LE",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.Def.Words.Seq_interpretation_Tm_arrow_32c83d7dfb0acafa0853c18310eaef3e",
        "Vale.Def.Words.Seq_interpretation_Tm_arrow_f190567c0e1fa3ea695a387828243344",
        "equation_Prims.nat", "equation_Vale.Def.Words.Four_s.four_select",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524",
        "interpretation_Tm_abs_4d71202e4ba071eb1eb9023f14fa665d",
        "interpretation_Tm_abs_595fd624207608dd886b2e84a81a518b",
        "interpretation_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_96d5057c16747c54e40078129bdefb54",
        "refinement_interpretation_Tm_refine_a8ed1c32215ef7054758d7b9026da0dd",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_e1f5e45cb61463bd8d5304890121db69",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524",
        "typing_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34"
      ],
      0,
      "c459a78f31e5729794c95a9dc41a1c29"
    ],
    [
      "Vale.Def.Words.Seq.seq_to_seq_four_to_seq_BE",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "dc565c4a92691a3178065b1cc6f48eb7"
    ],
    [
      "Vale.Def.Words.Seq.seq_to_seq_four_to_seq_BE",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.Def.Words.Seq_interpretation_Tm_arrow_32c83d7dfb0acafa0853c18310eaef3e",
        "Vale.Def.Words.Seq_interpretation_Tm_arrow_f190567c0e1fa3ea695a387828243344",
        "equation_Prims.nat", "equation_Vale.Def.Words.Four_s.four_select",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_BE",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_BE",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_2fc6b3ab64c18b145a616e44e8d8d874",
        "interpretation_Tm_abs_68712397230d19f3062e360c964e25da",
        "interpretation_Tm_abs_9cd3a42bbbd0f67ce68082a0bbce4cf2",
        "interpretation_Tm_abs_df2053a244470cdb2ac13b7c0c00e093",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_96d5057c16747c54e40078129bdefb54",
        "refinement_interpretation_Tm_refine_a8ed1c32215ef7054758d7b9026da0dd",
        "refinement_interpretation_Tm_refine_abd944e669f79e6af0f86cf95ccb27ea",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_2fc6b3ab64c18b145a616e44e8d8d874",
        "typing_Tm_abs_68712397230d19f3062e360c964e25da",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_BE"
      ],
      0,
      "88cffd22fc146ab4b8bbb23f5cf9f8a4"
    ],
    [
      "Vale.Def.Words.Seq.seq_four_to_seq_to_seq_four_LE",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "a1774ef13b86231228b9848023cc974e"
    ],
    [
      "Vale.Def.Words.Seq.seq_four_to_seq_to_seq_four_LE",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.Def.Words.Seq_interpretation_Tm_arrow_32c83d7dfb0acafa0853c18310eaef3e",
        "Vale.Def.Words.Seq_interpretation_Tm_arrow_f190567c0e1fa3ea695a387828243344",
        "equation_Prims.nat", "equation_Vale.Def.Words.Four_s.four_select",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524",
        "interpretation_Tm_abs_4d71202e4ba071eb1eb9023f14fa665d",
        "interpretation_Tm_abs_595fd624207608dd886b2e84a81a518b",
        "interpretation_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_96d5057c16747c54e40078129bdefb54",
        "refinement_interpretation_Tm_refine_a8ed1c32215ef7054758d7b9026da0dd",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524",
        "typing_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "af7a6fb08d616e72c49c4e2b138d66f6"
    ],
    [
      "Vale.Def.Words.Seq.lemma_fundamental_div_mod_4",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "276c5a89dd9521d8a5ca1e5865c11d50"
    ],
    [
      "Vale.Def.Words.Seq.four_to_nat_to_four_8",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "08999125b0190fa3879cb2b4ba60b487"
    ],
    [
      "Vale.Def.Words.Seq.four_to_nat_to_four_8",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "a08e3646f75d65b478aa506dffa0ac99"
    ],
    [
      "Vale.Def.Words.Seq.nat_to_four_to_nat",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "e9281c3dcb6f4a34157b8d26f85ad9e0"
    ],
    [
      "Vale.Def.Words.Seq.nat_to_four_to_nat",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "49c7b99cd93d5f9c21ca40caa550a248"
    ],
    [
      "Vale.Def.Words.Seq.four_to_seq_to_four_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
        "equation_Vale.Def.Words.Seq_s.seqn", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
        "typing_Vale.Def.Words.Seq_s.seq_to_four_LE"
      ],
      0,
      "89849c375358a3aa177b0f87902d9b1c"
    ],
    [
      "Vale.Def.Words.Seq.seq_to_four_to_seq_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_LE"
      ],
      0,
      "7a0ebdca99b4f7a3295c0b3d518b1f89"
    ],
    [
      "Vale.Def.Words.Seq.four_to_seq_to_four_BE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_to_four_BE",
        "equation_Vale.Def.Words.Seq_s.seqn", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
        "typing_Vale.Def.Words.Seq_s.seq_to_four_BE"
      ],
      0,
      "2013eed0fd72107817dcfff75d540255"
    ],
    [
      "Vale.Def.Words.Seq.seq_to_four_to_seq_BE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.Def.Words.Seq_s.seq_to_four_BE",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_BE"
      ],
      0,
      "f72efcce0404c17f7b59e10ee7040ef5"
    ],
    [
      "Vale.Def.Words.Seq.four_to_seq_LE_is_seq_four_to_seq_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
      ],
      0,
      "9ec201d7dd5a00a97d31faa3994d39fd"
    ],
    [
      "Vale.Def.Words.Seq.four_to_seq_LE_is_seq_four_to_seq_LE",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.Def.Words.Seq_interpretation_Tm_arrow_32c83d7dfb0acafa0853c18310eaef3e",
        "equation_Prims.nat", "equation_Vale.Def.Words.Four_s.four_select",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_595fd624207608dd886b2e84a81a518b",
        "interpretation_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_a8ed1c32215ef7054758d7b9026da0dd",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "aa75cb5ed22e0c42d2fdf2ce25a73fc4"
    ],
    [
      "Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "equation_Prims.nat",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "kinding_Vale.Def.Words_s.four@tok",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "0bac225869487d97b60052b09861595c"
    ],
    [
      "Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "equation_Prims.nat",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_FStar.Seq.Base.index",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8",
        "lemma_Vale.Def.Words.Seq.seq_to_seq_four_to_seq_LE",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_FStar.Seq.Base.index",
        "token_correspondence_Vale.Def.Words.Four_s.four_to_nat",
        "token_correspondence_Vale.Def.Words.Four_s.nat_to_four",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.init",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "c8ddda62e57d78e48e4b0f0caffdfb91"
    ],
    [
      "Vale.Def.Words.Seq.seq_nat32_to_seq_nat8_to_seq_nat32_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.Def.Words.Seq_interpretation_Tm_arrow_4217d864395e427d3d50043a7013186f",
        "Vale.Def.Words.Seq_interpretation_Tm_arrow_d99575c656699ec1bf0db12d4bfb9bae",
        "Vale.Def.Words.Seq_interpretation_Tm_arrow_efe96bb9514bece12be080c2a3348ae5",
        "constructor_distinct_Tm_unit", "equation_Prims.nat",
        "equation_Vale.Def.Words.Four_s.four_select",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_FStar.Seq.Base.index",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "interpretation_Tm_abs_4f03474956a6a2311e7d7bb19e902da5",
        "interpretation_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
        "interpretation_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
        "interpretation_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_Vale.Def.Words.Seq.nat_to_four_to_nat",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
        "refinement_interpretation_Tm_refine_528966909e656beff90629dc95073b2d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b75956299d71331caf39bdc95ee7a81c",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
        "refinement_interpretation_Tm_refine_f21dd5802eb4c999bcae09802023d5fd",
        "token_correspondence_FStar.Seq.Base.index",
        "token_correspondence_Vale.Def.Words.Four_s.four_to_nat",
        "token_correspondence_Vale.Def.Words.Four_s.nat_to_four",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.init",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Tm_abs_4f03474956a6a2311e7d7bb19e902da5",
        "typing_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
        "typing_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac",
        "typing_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "8eb0ffb72dba87db380b8dc5b409c863"
    ],
    [
      "Vale.Def.Words.Seq.seq_nat8_to_seq_uint8_to_seq_nat8",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "FStar.UInt8_pretyping_512f0e4172b97206a8b0e16196475713",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_FStar.Seq.Base.index",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.UInt8.uv_inv",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_FStar.Seq.Base.index",
        "token_correspondence_FStar.UInt8.uint_to_t",
        "token_correspondence_FStar.UInt8.v", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8"
      ],
      0,
      "d3df9a945a0f1606e35ed7c19ffbb7e3"
    ],
    [
      "Vale.Def.Words.Seq.seq_uint8_to_seq_nat8_to_seq_uint8",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_FStar.Seq.Base.index",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt8.vu_inv",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_FStar.Seq.Base.index",
        "token_correspondence_FStar.UInt8.uint_to_t",
        "token_correspondence_FStar.UInt8.v", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8"
      ],
      0,
      "e003ba3972a430b58c641f5f55ace939"
    ],
    [
      "Vale.Def.Words.Seq.seq_nat8_to_seq_uint8_injective",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt8.vu_inv",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt8.t",
        "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8"
      ],
      0,
      "641b0a02b838e5dec9a605dc0bca03bf"
    ],
    [
      "Vale.Def.Words.Seq.seq_four_to_seq_LE_injective",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "622be686a9101951ff965a638d384c85"
    ],
    [
      "Vale.Def.Words.Seq.seq_four_to_seq_LE_injective",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_Vale.Def.Words_s.four__uu___haseq",
        "equation_Prims.eqtype", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.hasEq_lemma",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "6334bcf967fa82d9bdff5350fe3456d1"
    ],
    [
      "Vale.Def.Words.Seq.seq_four_to_seq_LE_injective_specific",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "d23bb5d028bab45373ae601f24384f37"
    ],
    [
      "Vale.Def.Words.Seq.seq_four_to_seq_LE_injective_specific",
      2,
      1,
      0,
      [ "@query" ],
      0,
      "e3a8eaef8cd500bcb221671bccfad0c6"
    ],
    [
      "Vale.Def.Words.Seq.four_to_seq_LE_injective",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_Vale.Def.Words_s.four__uu___haseq",
        "equation_Prims.eqtype", "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "haseqTm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "lemma_FStar.Seq.Base.hasEq_lemma",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "73948f85666231700ffb09981fe2f522"
    ],
    [
      "Vale.Def.Words.Seq.four_to_nat_8_injective",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "d448ff0ece0c9d0adee25275b64ce46e"
    ],
    [
      "Vale.Def.Words.Seq.four_to_nat_8_injective",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "assumption_Vale.Def.Words_s.four__uu___haseq",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_typing",
        "lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "9597d8582164f7eb4f7086111f678a3f"
    ],
    [
      "Vale.Def.Words.Seq.nat_to_four_8_injective",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "2ec6b49f349c5f12678132751d86d6af"
    ],
    [
      "Vale.Def.Words.Seq.nat_to_four_8_injective",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "assumption_Vale.Def.Words_s.four__uu___haseq",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "f2f14a5887f65cb90e7f353176d85748"
    ],
    [
      "Vale.Def.Words.Seq.append_distributes_seq_to_seq_four_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Base.op_At_Bar",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac"
      ],
      0,
      "871cb978f53e4d92eeb328b0c9e8aa5f"
    ],
    [
      "Vale.Def.Words.Seq.append_distributes_seq_to_seq_four_LE",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.Def.Words.Seq_interpretation_Tm_arrow_f190567c0e1fa3ea695a387828243344",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524",
        "interpretation_Tm_abs_4d71202e4ba071eb1eb9023f14fa665d",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_387c17e1c2128da0ffe38534dd5bf717",
        "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_96d5057c16747c54e40078129bdefb54",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar",
        "typing_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "530bb96f577eb980fac80bc098dd1717"
    ],
    [
      "Vale.Def.Words.Seq.append_distributes_seq_four_to_seq_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.Def.Words.Seq_interpretation_Tm_arrow_32c83d7dfb0acafa0853c18310eaef3e",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_595fd624207608dd886b2e84a81a518b",
        "interpretation_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a8ed1c32215ef7054758d7b9026da0dd",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar",
        "typing_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "d6cd150d84955213e2ab7167c26b3bf6"
    ]
  ]
]