From 40d34ec3d79333358c6c3c21928eb7b8e6968912 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Mon, 2 Nov 2020 16:38:50 +0100
Subject: [PATCH] remove array iterator

---
 examples/mutable_map.c                        |   16 +-
 examples/proofs/mutable_map/generated_code.v  | 1062 ++++++++---------
 .../mutable_map/generated_proof_fsm_init.v    |    5 +-
 ...generated_proof_fsm_realloc_if_necessary.v |    7 +-
 theories/lang/base.v                          |    4 +
 theories/lithium/simpl_instances.v            |   12 +-
 theories/typing/array.v                       |   77 --
 theories/typing/automation/normalize.v        |    5 +-
 8 files changed, 558 insertions(+), 630 deletions(-)

diff --git a/examples/mutable_map.c b/examples/mutable_map.c
index e6ffdf86..43e4cb6e 100644
--- a/examples/mutable_map.c
+++ b/examples/mutable_map.c
@@ -70,8 +70,9 @@ void fsm_realloc_if_necessary(struct fixed_size_map *m);
 [[rc::requires("[alloc_initialized]")]]
 [[rc::ensures("m @ &own<{∅, replicate len Empty, len} @ fixed_size_map> ")]]
  [[rc::lemmas("fsm_invariant_init")]]
+ [[rc::tactics("all: try by apply/list_subequiv_split; solve_goal.")]]
  [[rc::tactics("all: try by rewrite length_filter_replicate_True; solve_goal.")]]
- [[rc::tactics("all: try by f_equal; solve_goal.")]]
+ [[rc::tactics("all: try by rewrite !replicate_O; solve_goal.")]]
 void fsm_init(struct fixed_size_map *m, size_t len) {
   size_t i;
   void *storage = alloc_array(sizeof(struct item), len);
@@ -81,9 +82,9 @@ void fsm_init(struct fixed_size_map *m, size_t len) {
 
   [[rc::exists("i : nat")]]
   [[rc::inv_vars("i : i @ int<size_t>")]]
-  [[rc::inv_vars("m : m @ &own<struct<struct_fixed_size_map, &own<array_iterator<" \
-                "struct_item, i, len, {replicate i Empty `at_type` item}," \
-                 "uninit<struct_item>, {replicate (len - i)%nat (uninit (struct_item))}>>, len @ int<size_t>, len @ int<size_t>>> ")]]
+  [[rc::inv_vars("m : m @ &own<struct<struct_fixed_size_map, &own<array<struct_item," \
+                "{replicate i Empty `at_type` item ++ replicate (len - i)%nat (uninit (struct_item))}>>," \
+                 "len @ int<size_t>, len @ int<size_t>>>")]]
   [[rc::constraints("{i <= len}")]]
   for(i = 0; i < len; i += 1) {
     (*m->items)[i].tag = ITEM_EMPTY;
@@ -213,12 +214,7 @@ size_t compute_min_count(size_t len) {
  [[rc::tactics("all: try by apply: fsm_copy_entries_not_add; solve_goal.")]]
  [[rc::tactics("all: try by apply: fsm_copy_entries_add; solve_goal.")]]
  [[rc::tactics("all: try by apply: fsm_copy_entries_id; solve_goal.")]]
- [[rc::tactics("all: try (apply list_subequiv_split; [solve_goal|]).")]]
- [[rc::tactics("all: try rewrite !firstn_app !take_replicate !skipn_app !drop_replicate !replicate_length !fmap_drop !drop_drop -minus_n_n.")]]
- [[rc::tactics("all: try split; f_equal.")]]
- [[rc::tactics("all: try by f_equal; lia.")]]
- [[rc::tactics("all: try have ->:(i - (i + 1) = 0)%nat by lia.")]]
- [[rc::tactics("all: try by rewrite !firstn_O.")]]
+ [[rc::tactics("all: try by apply list_subequiv_split; [solve_goal|]; normalize_and_simpl_goal; try solve_goal; f_equal; solve_goal.")]]
 void fsm_realloc_if_necessary(struct fixed_size_map *m) {
   if(compute_min_count(m->length) <= m->count) {
     return;
diff --git a/examples/proofs/mutable_map/generated_code.v b/examples/proofs/mutable_map/generated_code.v
index a1c993ca..260e3101 100644
--- a/examples/proofs/mutable_map/generated_code.v
+++ b/examples/proofs/mutable_map/generated_code.v
@@ -6,537 +6,537 @@ Set Default Proof Using "Type".
 (* Generated from [examples/mutable_map.c]. *)
 Section code.
   Definition file_0 : string := "examples/mutable_map.c".
-  Definition loc_2 : location_info := LocationInfo file_0 223 2 225 3.
-  Definition loc_3 : location_info := LocationInfo file_0 227 2 227 89.
-  Definition loc_4 : location_info := LocationInfo file_0 230 2 230 33.
-  Definition loc_5 : location_info := LocationInfo file_0 232 2 232 25.
-  Definition loc_6 : location_info := LocationInfo file_0 240 2 245 3.
-  Definition loc_7 : location_info := LocationInfo file_0 240 2 245 3.
-  Definition loc_8 : location_info := LocationInfo file_0 240 2 245 3.
-  Definition loc_9 : location_info := LocationInfo file_0 246 2 246 55.
-  Definition loc_10 : location_info := LocationInfo file_0 247 2 247 10.
-  Definition loc_11 : location_info := LocationInfo file_0 247 2 247 4.
-  Definition loc_12 : location_info := LocationInfo file_0 247 3 247 4.
-  Definition loc_13 : location_info := LocationInfo file_0 247 3 247 4.
-  Definition loc_14 : location_info := LocationInfo file_0 247 7 247 9.
-  Definition loc_15 : location_info := LocationInfo file_0 247 7 247 9.
-  Definition loc_16 : location_info := LocationInfo file_0 246 2 246 12.
-  Definition loc_17 : location_info := LocationInfo file_0 246 2 246 12.
-  Definition loc_18 : location_info := LocationInfo file_0 246 13 246 32.
-  Definition loc_19 : location_info := LocationInfo file_0 246 34 246 43.
-  Definition loc_20 : location_info := LocationInfo file_0 246 34 246 43.
-  Definition loc_21 : location_info := LocationInfo file_0 246 34 246 35.
-  Definition loc_22 : location_info := LocationInfo file_0 246 34 246 35.
-  Definition loc_23 : location_info := LocationInfo file_0 246 45 246 53.
-  Definition loc_24 : location_info := LocationInfo file_0 246 45 246 53.
-  Definition loc_25 : location_info := LocationInfo file_0 246 45 246 46.
-  Definition loc_26 : location_info := LocationInfo file_0 246 45 246 46.
-  Definition loc_27 : location_info := LocationInfo file_0 240 43 245 3.
-  Definition loc_28 : location_info := LocationInfo file_0 241 4 243 5.
-  Definition loc_29 : location_info := LocationInfo file_0 244 4 244 17.
-  Definition loc_30 : location_info := LocationInfo file_0 244 17 244 5.
-  Definition loc_31 : location_info := LocationInfo file_0 240 2 245 3.
-  Definition loc_33 : location_info := LocationInfo file_0 240 35 240 36.
-  Definition loc_34 : location_info := LocationInfo file_0 240 35 240 41.
-  Definition loc_35 : location_info := LocationInfo file_0 240 35 240 36.
-  Definition loc_36 : location_info := LocationInfo file_0 240 35 240 36.
-  Definition loc_37 : location_info := LocationInfo file_0 240 40 240 41.
-  Definition loc_38 : location_info := LocationInfo file_0 244 4 244 16.
-  Definition loc_39 : location_info := LocationInfo file_0 244 5 244 16.
-  Definition loc_40 : location_info := LocationInfo file_0 244 6 244 8.
-  Definition loc_41 : location_info := LocationInfo file_0 241 42 243 5.
-  Definition loc_42 : location_info := LocationInfo file_0 242 6 242 80.
-  Definition loc_43 : location_info := LocationInfo file_0 242 6 242 16.
-  Definition loc_44 : location_info := LocationInfo file_0 242 6 242 16.
-  Definition loc_45 : location_info := LocationInfo file_0 242 17 242 20.
-  Definition loc_46 : location_info := LocationInfo file_0 242 18 242 20.
-  Definition loc_47 : location_info := LocationInfo file_0 242 22 242 48.
-  Definition loc_48 : location_info := LocationInfo file_0 242 22 242 48.
-  Definition loc_49 : location_info := LocationInfo file_0 242 22 242 44.
-  Definition loc_50 : location_info := LocationInfo file_0 242 22 242 38.
-  Definition loc_51 : location_info := LocationInfo file_0 242 22 242 36.
-  Definition loc_52 : location_info := LocationInfo file_0 242 22 242 36.
-  Definition loc_53 : location_info := LocationInfo file_0 242 22 242 33.
-  Definition loc_54 : location_info := LocationInfo file_0 242 22 242 33.
-  Definition loc_55 : location_info := LocationInfo file_0 242 24 242 32.
-  Definition loc_56 : location_info := LocationInfo file_0 242 24 242 32.
-  Definition loc_57 : location_info := LocationInfo file_0 242 24 242 25.
-  Definition loc_58 : location_info := LocationInfo file_0 242 24 242 25.
-  Definition loc_59 : location_info := LocationInfo file_0 242 34 242 35.
-  Definition loc_60 : location_info := LocationInfo file_0 242 34 242 35.
-  Definition loc_61 : location_info := LocationInfo file_0 242 50 242 78.
-  Definition loc_62 : location_info := LocationInfo file_0 242 50 242 78.
-  Definition loc_63 : location_info := LocationInfo file_0 242 50 242 72.
-  Definition loc_64 : location_info := LocationInfo file_0 242 50 242 66.
-  Definition loc_65 : location_info := LocationInfo file_0 242 50 242 64.
-  Definition loc_66 : location_info := LocationInfo file_0 242 50 242 64.
-  Definition loc_67 : location_info := LocationInfo file_0 242 50 242 61.
-  Definition loc_68 : location_info := LocationInfo file_0 242 50 242 61.
-  Definition loc_69 : location_info := LocationInfo file_0 242 52 242 60.
-  Definition loc_70 : location_info := LocationInfo file_0 242 52 242 60.
-  Definition loc_71 : location_info := LocationInfo file_0 242 52 242 53.
-  Definition loc_72 : location_info := LocationInfo file_0 242 52 242 53.
-  Definition loc_73 : location_info := LocationInfo file_0 242 62 242 63.
-  Definition loc_74 : location_info := LocationInfo file_0 242 62 242 63.
-  Definition loc_76 : location_info := LocationInfo file_0 241 7 241 40.
-  Definition loc_77 : location_info := LocationInfo file_0 241 7 241 25.
-  Definition loc_78 : location_info := LocationInfo file_0 241 7 241 25.
-  Definition loc_79 : location_info := LocationInfo file_0 241 7 241 21.
-  Definition loc_80 : location_info := LocationInfo file_0 241 7 241 21.
-  Definition loc_81 : location_info := LocationInfo file_0 241 7 241 18.
-  Definition loc_82 : location_info := LocationInfo file_0 241 7 241 18.
-  Definition loc_83 : location_info := LocationInfo file_0 241 9 241 17.
-  Definition loc_84 : location_info := LocationInfo file_0 241 9 241 17.
-  Definition loc_85 : location_info := LocationInfo file_0 241 9 241 10.
-  Definition loc_86 : location_info := LocationInfo file_0 241 9 241 10.
-  Definition loc_87 : location_info := LocationInfo file_0 241 19 241 20.
-  Definition loc_88 : location_info := LocationInfo file_0 241 19 241 20.
-  Definition loc_89 : location_info := LocationInfo file_0 241 29 241 40.
-  Definition loc_90 : location_info := LocationInfo file_0 241 38 241 39.
-  Definition loc_91 : location_info := LocationInfo file_0 240 20 240 33.
-  Definition loc_92 : location_info := LocationInfo file_0 240 20 240 21.
-  Definition loc_93 : location_info := LocationInfo file_0 240 20 240 21.
-  Definition loc_94 : location_info := LocationInfo file_0 240 24 240 33.
-  Definition loc_95 : location_info := LocationInfo file_0 240 24 240 33.
-  Definition loc_96 : location_info := LocationInfo file_0 240 24 240 25.
-  Definition loc_97 : location_info := LocationInfo file_0 240 24 240 25.
-  Definition loc_98 : location_info := LocationInfo file_0 240 17 240 18.
-  Definition loc_101 : location_info := LocationInfo file_0 232 2 232 10.
-  Definition loc_102 : location_info := LocationInfo file_0 232 2 232 10.
-  Definition loc_103 : location_info := LocationInfo file_0 232 11 232 14.
-  Definition loc_104 : location_info := LocationInfo file_0 232 12 232 14.
-  Definition loc_105 : location_info := LocationInfo file_0 232 16 232 23.
-  Definition loc_106 : location_info := LocationInfo file_0 232 16 232 23.
-  Definition loc_107 : location_info := LocationInfo file_0 230 19 230 32.
-  Definition loc_108 : location_info := LocationInfo file_0 230 19 230 28.
-  Definition loc_109 : location_info := LocationInfo file_0 230 19 230 28.
-  Definition loc_110 : location_info := LocationInfo file_0 230 19 230 20.
-  Definition loc_111 : location_info := LocationInfo file_0 230 19 230 20.
-  Definition loc_112 : location_info := LocationInfo file_0 230 31 230 32.
-  Definition loc_115 : location_info := LocationInfo file_0 227 68 227 70.
-  Definition loc_116 : location_info := LocationInfo file_0 227 76 227 89.
-  Definition loc_117 : location_info := LocationInfo file_0 227 78 227 87.
-  Definition loc_118 : location_info := LocationInfo file_0 227 78 227 87.
-  Definition loc_119 : location_info := LocationInfo file_0 227 86 227 87.
-  Definition loc_120 : location_info := LocationInfo file_0 227 78 227 87.
-  Definition loc_121 : location_info := LocationInfo file_0 227 78 227 87.
-  Definition loc_122 : location_info := LocationInfo file_0 227 84 227 85.
-  Definition loc_123 : location_info := LocationInfo file_0 227 5 227 66.
-  Definition loc_124 : location_info := LocationInfo file_0 227 5 227 14.
-  Definition loc_125 : location_info := LocationInfo file_0 227 5 227 14.
-  Definition loc_126 : location_info := LocationInfo file_0 227 5 227 6.
-  Definition loc_127 : location_info := LocationInfo file_0 227 5 227 6.
-  Definition loc_128 : location_info := LocationInfo file_0 227 17 227 66.
-  Definition loc_129 : location_info := LocationInfo file_0 227 17 227 61.
-  Definition loc_130 : location_info := LocationInfo file_0 227 17 227 39.
-  Definition loc_131 : location_info := LocationInfo file_0 227 17 227 35.
-  Definition loc_132 : location_info := LocationInfo file_0 227 38 227 39.
-  Definition loc_133 : location_info := LocationInfo file_0 227 42 227 61.
-  Definition loc_134 : location_info := LocationInfo file_0 227 64 227 66.
-  Definition loc_135 : location_info := LocationInfo file_0 223 47 225 3.
-  Definition loc_136 : location_info := LocationInfo file_0 224 4 224 11.
-  Definition loc_139 : location_info := LocationInfo file_0 223 5 223 45.
-  Definition loc_140 : location_info := LocationInfo file_0 223 5 223 33.
-  Definition loc_141 : location_info := LocationInfo file_0 223 5 223 22.
-  Definition loc_142 : location_info := LocationInfo file_0 223 5 223 22.
-  Definition loc_143 : location_info := LocationInfo file_0 223 23 223 32.
-  Definition loc_144 : location_info := LocationInfo file_0 223 23 223 32.
-  Definition loc_145 : location_info := LocationInfo file_0 223 23 223 24.
-  Definition loc_146 : location_info := LocationInfo file_0 223 23 223 24.
-  Definition loc_147 : location_info := LocationInfo file_0 223 37 223 45.
-  Definition loc_148 : location_info := LocationInfo file_0 223 37 223 45.
-  Definition loc_149 : location_info := LocationInfo file_0 223 37 223 38.
-  Definition loc_150 : location_info := LocationInfo file_0 223 37 223 38.
-  Definition loc_153 : location_info := LocationInfo file_0 77 2 77 56.
-  Definition loc_154 : location_info := LocationInfo file_0 78 2 78 18.
-  Definition loc_155 : location_info := LocationInfo file_0 79 2 79 21.
-  Definition loc_156 : location_info := LocationInfo file_0 80 2 80 17.
-  Definition loc_157 : location_info := LocationInfo file_0 88 2 91 3.
-  Definition loc_158 : location_info := LocationInfo file_0 88 6 88 11.
-  Definition loc_159 : location_info := LocationInfo file_0 88 2 91 3.
-  Definition loc_160 : location_info := LocationInfo file_0 88 30 91 3.
-  Definition loc_161 : location_info := LocationInfo file_0 89 4 89 37.
-  Definition loc_162 : location_info := LocationInfo file_0 90 4 90 37.
-  Definition loc_163 : location_info := LocationInfo file_0 88 2 91 3.
-  Definition loc_164 : location_info := LocationInfo file_0 88 22 88 28.
-  Definition loc_165 : location_info := LocationInfo file_0 88 22 88 23.
-  Definition loc_166 : location_info := LocationInfo file_0 88 22 88 28.
-  Definition loc_167 : location_info := LocationInfo file_0 88 22 88 23.
-  Definition loc_168 : location_info := LocationInfo file_0 88 22 88 23.
-  Definition loc_169 : location_info := LocationInfo file_0 88 27 88 28.
-  Definition loc_170 : location_info := LocationInfo file_0 90 4 90 32.
-  Definition loc_171 : location_info := LocationInfo file_0 90 4 90 26.
-  Definition loc_172 : location_info := LocationInfo file_0 90 4 90 20.
-  Definition loc_173 : location_info := LocationInfo file_0 90 4 90 18.
-  Definition loc_174 : location_info := LocationInfo file_0 90 4 90 18.
-  Definition loc_175 : location_info := LocationInfo file_0 90 4 90 15.
-  Definition loc_176 : location_info := LocationInfo file_0 90 4 90 15.
-  Definition loc_177 : location_info := LocationInfo file_0 90 6 90 14.
-  Definition loc_178 : location_info := LocationInfo file_0 90 6 90 14.
-  Definition loc_179 : location_info := LocationInfo file_0 90 6 90 7.
-  Definition loc_180 : location_info := LocationInfo file_0 90 6 90 7.
-  Definition loc_181 : location_info := LocationInfo file_0 90 16 90 17.
-  Definition loc_182 : location_info := LocationInfo file_0 90 16 90 17.
-  Definition loc_183 : location_info := LocationInfo file_0 90 35 90 36.
-  Definition loc_184 : location_info := LocationInfo file_0 89 4 89 22.
-  Definition loc_185 : location_info := LocationInfo file_0 89 4 89 18.
-  Definition loc_186 : location_info := LocationInfo file_0 89 4 89 18.
-  Definition loc_187 : location_info := LocationInfo file_0 89 4 89 15.
-  Definition loc_188 : location_info := LocationInfo file_0 89 4 89 15.
-  Definition loc_189 : location_info := LocationInfo file_0 89 6 89 14.
-  Definition loc_190 : location_info := LocationInfo file_0 89 6 89 14.
-  Definition loc_191 : location_info := LocationInfo file_0 89 6 89 7.
-  Definition loc_192 : location_info := LocationInfo file_0 89 6 89 7.
-  Definition loc_193 : location_info := LocationInfo file_0 89 16 89 17.
-  Definition loc_194 : location_info := LocationInfo file_0 89 16 89 17.
-  Definition loc_195 : location_info := LocationInfo file_0 89 25 89 36.
-  Definition loc_196 : location_info := LocationInfo file_0 89 34 89 35.
-  Definition loc_197 : location_info := LocationInfo file_0 88 13 88 20.
-  Definition loc_198 : location_info := LocationInfo file_0 88 13 88 14.
-  Definition loc_199 : location_info := LocationInfo file_0 88 13 88 14.
-  Definition loc_200 : location_info := LocationInfo file_0 88 17 88 20.
-  Definition loc_201 : location_info := LocationInfo file_0 88 17 88 20.
-  Definition loc_202 : location_info := LocationInfo file_0 88 6 88 7.
-  Definition loc_203 : location_info := LocationInfo file_0 88 10 88 11.
-  Definition loc_204 : location_info := LocationInfo file_0 80 2 80 10.
-  Definition loc_205 : location_info := LocationInfo file_0 80 2 80 3.
-  Definition loc_206 : location_info := LocationInfo file_0 80 2 80 3.
-  Definition loc_207 : location_info := LocationInfo file_0 80 13 80 16.
-  Definition loc_208 : location_info := LocationInfo file_0 80 13 80 16.
-  Definition loc_209 : location_info := LocationInfo file_0 79 2 79 10.
-  Definition loc_210 : location_info := LocationInfo file_0 79 2 79 3.
-  Definition loc_211 : location_info := LocationInfo file_0 79 2 79 3.
-  Definition loc_212 : location_info := LocationInfo file_0 79 13 79 20.
-  Definition loc_213 : location_info := LocationInfo file_0 79 13 79 20.
-  Definition loc_214 : location_info := LocationInfo file_0 78 2 78 11.
-  Definition loc_215 : location_info := LocationInfo file_0 78 2 78 3.
-  Definition loc_216 : location_info := LocationInfo file_0 78 2 78 3.
-  Definition loc_217 : location_info := LocationInfo file_0 78 14 78 17.
-  Definition loc_218 : location_info := LocationInfo file_0 78 14 78 17.
-  Definition loc_219 : location_info := LocationInfo file_0 77 18 77 55.
-  Definition loc_220 : location_info := LocationInfo file_0 77 18 77 29.
-  Definition loc_221 : location_info := LocationInfo file_0 77 18 77 29.
-  Definition loc_222 : location_info := LocationInfo file_0 77 30 77 49.
-  Definition loc_223 : location_info := LocationInfo file_0 77 51 77 54.
-  Definition loc_224 : location_info := LocationInfo file_0 77 51 77 54.
-  Definition loc_229 : location_info := LocationInfo file_0 102 4 102 21.
-  Definition loc_230 : location_info := LocationInfo file_0 102 11 102 20.
-  Definition loc_231 : location_info := LocationInfo file_0 102 11 102 14.
-  Definition loc_232 : location_info := LocationInfo file_0 102 11 102 14.
-  Definition loc_233 : location_info := LocationInfo file_0 102 17 102 20.
-  Definition loc_234 : location_info := LocationInfo file_0 102 17 102 20.
-  Definition loc_237 : location_info := LocationInfo file_0 115 4 115 55.
-  Definition loc_238 : location_info := LocationInfo file_0 121 4 130 5.
-  Definition loc_239 : location_info := LocationInfo file_0 121 4 130 5.
-  Definition loc_240 : location_info := LocationInfo file_0 121 13 130 5.
-  Definition loc_241 : location_info := LocationInfo file_0 122 8 124 9.
-  Definition loc_242 : location_info := LocationInfo file_0 125 8 127 9.
-  Definition loc_243 : location_info := LocationInfo file_0 128 8 128 22.
-  Definition loc_244 : location_info := LocationInfo file_0 128 22 128 9.
-  Definition loc_245 : location_info := LocationInfo file_0 129 8 129 46.
-  Definition loc_246 : location_info := LocationInfo file_0 121 4 130 5.
-  Definition loc_247 : location_info := LocationInfo file_0 121 4 130 5.
-  Definition loc_248 : location_info := LocationInfo file_0 129 8 129 16.
-  Definition loc_249 : location_info := LocationInfo file_0 129 19 129 45.
-  Definition loc_250 : location_info := LocationInfo file_0 129 19 129 33.
-  Definition loc_251 : location_info := LocationInfo file_0 129 20 129 28.
-  Definition loc_252 : location_info := LocationInfo file_0 129 20 129 28.
-  Definition loc_253 : location_info := LocationInfo file_0 129 31 129 32.
-  Definition loc_254 : location_info := LocationInfo file_0 129 36 129 45.
-  Definition loc_255 : location_info := LocationInfo file_0 129 36 129 45.
-  Definition loc_256 : location_info := LocationInfo file_0 129 36 129 37.
-  Definition loc_257 : location_info := LocationInfo file_0 129 36 129 37.
-  Definition loc_258 : location_info := LocationInfo file_0 128 8 128 21.
-  Definition loc_259 : location_info := LocationInfo file_0 128 8 128 17.
-  Definition loc_260 : location_info := LocationInfo file_0 128 8 128 17.
-  Definition loc_261 : location_info := LocationInfo file_0 128 8 128 9.
-  Definition loc_262 : location_info := LocationInfo file_0 128 8 128 9.
-  Definition loc_263 : location_info := LocationInfo file_0 128 20 128 21.
-  Definition loc_264 : location_info := LocationInfo file_0 125 97 127 9.
-  Definition loc_265 : location_info := LocationInfo file_0 126 12 126 28.
-  Definition loc_266 : location_info := LocationInfo file_0 126 19 126 27.
-  Definition loc_267 : location_info := LocationInfo file_0 126 19 126 27.
-  Definition loc_270 : location_info := LocationInfo file_0 125 11 125 51.
-  Definition loc_271 : location_info := LocationInfo file_0 125 11 125 36.
-  Definition loc_272 : location_info := LocationInfo file_0 125 11 125 36.
-  Definition loc_273 : location_info := LocationInfo file_0 125 11 125 32.
-  Definition loc_274 : location_info := LocationInfo file_0 125 11 125 32.
-  Definition loc_275 : location_info := LocationInfo file_0 125 11 125 22.
-  Definition loc_276 : location_info := LocationInfo file_0 125 11 125 22.
-  Definition loc_277 : location_info := LocationInfo file_0 125 13 125 21.
-  Definition loc_278 : location_info := LocationInfo file_0 125 13 125 21.
-  Definition loc_279 : location_info := LocationInfo file_0 125 13 125 14.
-  Definition loc_280 : location_info := LocationInfo file_0 125 13 125 14.
-  Definition loc_281 : location_info := LocationInfo file_0 125 23 125 31.
-  Definition loc_282 : location_info := LocationInfo file_0 125 23 125 31.
-  Definition loc_283 : location_info := LocationInfo file_0 125 40 125 51.
-  Definition loc_284 : location_info := LocationInfo file_0 125 49 125 50.
-  Definition loc_285 : location_info := LocationInfo file_0 125 55 125 95.
-  Definition loc_286 : location_info := LocationInfo file_0 125 55 125 88.
-  Definition loc_287 : location_info := LocationInfo file_0 125 55 125 88.
-  Definition loc_288 : location_info := LocationInfo file_0 125 55 125 84.
-  Definition loc_289 : location_info := LocationInfo file_0 125 55 125 78.
-  Definition loc_290 : location_info := LocationInfo file_0 125 55 125 76.
-  Definition loc_291 : location_info := LocationInfo file_0 125 55 125 76.
-  Definition loc_292 : location_info := LocationInfo file_0 125 55 125 66.
-  Definition loc_293 : location_info := LocationInfo file_0 125 55 125 66.
-  Definition loc_294 : location_info := LocationInfo file_0 125 57 125 65.
-  Definition loc_295 : location_info := LocationInfo file_0 125 57 125 65.
-  Definition loc_296 : location_info := LocationInfo file_0 125 57 125 58.
-  Definition loc_297 : location_info := LocationInfo file_0 125 57 125 58.
-  Definition loc_298 : location_info := LocationInfo file_0 125 67 125 75.
-  Definition loc_299 : location_info := LocationInfo file_0 125 67 125 75.
-  Definition loc_300 : location_info := LocationInfo file_0 125 92 125 95.
-  Definition loc_301 : location_info := LocationInfo file_0 125 92 125 95.
-  Definition loc_302 : location_info := LocationInfo file_0 122 147 124 9.
-  Definition loc_303 : location_info := LocationInfo file_0 123 12 123 28.
-  Definition loc_304 : location_info := LocationInfo file_0 123 19 123 27.
-  Definition loc_305 : location_info := LocationInfo file_0 123 19 123 27.
-  Definition loc_308 : location_info := LocationInfo file_0 122 11 122 51.
-  Definition loc_309 : location_info := LocationInfo file_0 122 11 122 36.
-  Definition loc_310 : location_info := LocationInfo file_0 122 11 122 36.
-  Definition loc_311 : location_info := LocationInfo file_0 122 11 122 32.
-  Definition loc_312 : location_info := LocationInfo file_0 122 11 122 32.
-  Definition loc_313 : location_info := LocationInfo file_0 122 11 122 22.
-  Definition loc_314 : location_info := LocationInfo file_0 122 11 122 22.
-  Definition loc_315 : location_info := LocationInfo file_0 122 13 122 21.
-  Definition loc_316 : location_info := LocationInfo file_0 122 13 122 21.
-  Definition loc_317 : location_info := LocationInfo file_0 122 13 122 14.
-  Definition loc_318 : location_info := LocationInfo file_0 122 13 122 14.
-  Definition loc_319 : location_info := LocationInfo file_0 122 23 122 31.
-  Definition loc_320 : location_info := LocationInfo file_0 122 23 122 31.
-  Definition loc_321 : location_info := LocationInfo file_0 122 40 122 51.
-  Definition loc_322 : location_info := LocationInfo file_0 122 49 122 50.
-  Definition loc_324 : location_info := LocationInfo file_0 122 56 122 96.
-  Definition loc_325 : location_info := LocationInfo file_0 122 56 122 81.
-  Definition loc_326 : location_info := LocationInfo file_0 122 56 122 81.
-  Definition loc_327 : location_info := LocationInfo file_0 122 56 122 77.
-  Definition loc_328 : location_info := LocationInfo file_0 122 56 122 77.
-  Definition loc_329 : location_info := LocationInfo file_0 122 56 122 67.
-  Definition loc_330 : location_info := LocationInfo file_0 122 56 122 67.
-  Definition loc_331 : location_info := LocationInfo file_0 122 58 122 66.
-  Definition loc_332 : location_info := LocationInfo file_0 122 58 122 66.
-  Definition loc_333 : location_info := LocationInfo file_0 122 58 122 59.
-  Definition loc_334 : location_info := LocationInfo file_0 122 58 122 59.
-  Definition loc_335 : location_info := LocationInfo file_0 122 68 122 76.
-  Definition loc_336 : location_info := LocationInfo file_0 122 68 122 76.
-  Definition loc_337 : location_info := LocationInfo file_0 122 85 122 96.
-  Definition loc_338 : location_info := LocationInfo file_0 122 94 122 95.
-  Definition loc_339 : location_info := LocationInfo file_0 122 100 122 144.
-  Definition loc_340 : location_info := LocationInfo file_0 122 100 122 137.
-  Definition loc_341 : location_info := LocationInfo file_0 122 100 122 137.
-  Definition loc_342 : location_info := LocationInfo file_0 122 100 122 133.
-  Definition loc_343 : location_info := LocationInfo file_0 122 100 122 123.
-  Definition loc_344 : location_info := LocationInfo file_0 122 100 122 121.
-  Definition loc_345 : location_info := LocationInfo file_0 122 100 122 121.
-  Definition loc_346 : location_info := LocationInfo file_0 122 100 122 111.
-  Definition loc_347 : location_info := LocationInfo file_0 122 100 122 111.
-  Definition loc_348 : location_info := LocationInfo file_0 122 102 122 110.
-  Definition loc_349 : location_info := LocationInfo file_0 122 102 122 110.
-  Definition loc_350 : location_info := LocationInfo file_0 122 102 122 103.
-  Definition loc_351 : location_info := LocationInfo file_0 122 102 122 103.
-  Definition loc_352 : location_info := LocationInfo file_0 122 112 122 120.
-  Definition loc_353 : location_info := LocationInfo file_0 122 112 122 120.
-  Definition loc_354 : location_info := LocationInfo file_0 122 141 122 144.
-  Definition loc_355 : location_info := LocationInfo file_0 122 141 122 144.
-  Definition loc_356 : location_info := LocationInfo file_0 121 10 121 11.
-  Definition loc_357 : location_info := LocationInfo file_0 115 22 115 54.
-  Definition loc_358 : location_info := LocationInfo file_0 115 22 115 38.
-  Definition loc_359 : location_info := LocationInfo file_0 115 22 115 38.
-  Definition loc_360 : location_info := LocationInfo file_0 115 39 115 48.
-  Definition loc_361 : location_info := LocationInfo file_0 115 39 115 48.
-  Definition loc_362 : location_info := LocationInfo file_0 115 39 115 40.
-  Definition loc_363 : location_info := LocationInfo file_0 115 39 115 40.
-  Definition loc_364 : location_info := LocationInfo file_0 115 50 115 53.
-  Definition loc_365 : location_info := LocationInfo file_0 115 50 115 53.
-  Definition loc_370 : location_info := LocationInfo file_0 143 4 143 32.
-  Definition loc_371 : location_info := LocationInfo file_0 144 4 144 40.
-  Definition loc_372 : location_info := LocationInfo file_0 145 4 145 36.
-  Definition loc_373 : location_info := LocationInfo file_0 146 4 146 47.
-  Definition loc_374 : location_info := LocationInfo file_0 147 4 151 5.
-  Definition loc_375 : location_info := LocationInfo file_0 153 4 153 28.
-  Definition loc_376 : location_info := LocationInfo file_0 154 4 154 28.
-  Definition loc_377 : location_info := LocationInfo file_0 155 4 155 32.
-  Definition loc_378 : location_info := LocationInfo file_0 157 4 157 20.
-  Definition loc_379 : location_info := LocationInfo file_0 157 11 157 19.
-  Definition loc_380 : location_info := LocationInfo file_0 157 11 157 19.
-  Definition loc_381 : location_info := LocationInfo file_0 155 4 155 23.
-  Definition loc_382 : location_info := LocationInfo file_0 155 4 155 17.
-  Definition loc_383 : location_info := LocationInfo file_0 155 4 155 11.
-  Definition loc_384 : location_info := LocationInfo file_0 155 4 155 8.
-  Definition loc_385 : location_info := LocationInfo file_0 155 4 155 8.
-  Definition loc_386 : location_info := LocationInfo file_0 155 26 155 31.
-  Definition loc_387 : location_info := LocationInfo file_0 155 26 155 31.
-  Definition loc_388 : location_info := LocationInfo file_0 154 4 154 21.
-  Definition loc_389 : location_info := LocationInfo file_0 154 4 154 17.
-  Definition loc_390 : location_info := LocationInfo file_0 154 4 154 11.
-  Definition loc_391 : location_info := LocationInfo file_0 154 4 154 8.
-  Definition loc_392 : location_info := LocationInfo file_0 154 4 154 8.
-  Definition loc_393 : location_info := LocationInfo file_0 154 24 154 27.
-  Definition loc_394 : location_info := LocationInfo file_0 154 24 154 27.
-  Definition loc_395 : location_info := LocationInfo file_0 153 4 153 13.
-  Definition loc_396 : location_info := LocationInfo file_0 153 4 153 8.
-  Definition loc_397 : location_info := LocationInfo file_0 153 4 153 8.
-  Definition loc_398 : location_info := LocationInfo file_0 153 16 153 27.
-  Definition loc_399 : location_info := LocationInfo file_0 153 25 153 26.
-  Definition loc_400 : location_info := LocationInfo file_0 147 34 149 5.
-  Definition loc_401 : location_info := LocationInfo file_0 148 8 148 39.
-  Definition loc_402 : location_info := LocationInfo file_0 148 8 148 16.
-  Definition loc_403 : location_info := LocationInfo file_0 148 19 148 38.
-  Definition loc_404 : location_info := LocationInfo file_0 148 19 148 38.
-  Definition loc_405 : location_info := LocationInfo file_0 148 19 148 32.
-  Definition loc_406 : location_info := LocationInfo file_0 148 19 148 26.
-  Definition loc_407 : location_info := LocationInfo file_0 148 19 148 23.
-  Definition loc_408 : location_info := LocationInfo file_0 148 19 148 23.
-  Definition loc_409 : location_info := LocationInfo file_0 149 11 151 5.
-  Definition loc_410 : location_info := LocationInfo file_0 149 40 151 5.
-  Definition loc_411 : location_info := LocationInfo file_0 150 6 150 20.
-  Definition loc_412 : location_info := LocationInfo file_0 150 6 150 14.
-  Definition loc_413 : location_info := LocationInfo file_0 150 6 150 7.
-  Definition loc_414 : location_info := LocationInfo file_0 150 6 150 7.
-  Definition loc_415 : location_info := LocationInfo file_0 150 6 150 19.
-  Definition loc_416 : location_info := LocationInfo file_0 150 6 150 14.
-  Definition loc_417 : location_info := LocationInfo file_0 150 6 150 14.
-  Definition loc_418 : location_info := LocationInfo file_0 150 6 150 7.
-  Definition loc_419 : location_info := LocationInfo file_0 150 6 150 7.
-  Definition loc_420 : location_info := LocationInfo file_0 150 18 150 19.
-  Definition loc_422 : location_info := LocationInfo file_0 149 14 149 38.
-  Definition loc_423 : location_info := LocationInfo file_0 149 14 149 23.
-  Definition loc_424 : location_info := LocationInfo file_0 149 14 149 23.
-  Definition loc_425 : location_info := LocationInfo file_0 149 14 149 18.
-  Definition loc_426 : location_info := LocationInfo file_0 149 14 149 18.
-  Definition loc_427 : location_info := LocationInfo file_0 149 27 149 38.
-  Definition loc_428 : location_info := LocationInfo file_0 149 36 149 37.
-  Definition loc_429 : location_info := LocationInfo file_0 147 8 147 32.
-  Definition loc_430 : location_info := LocationInfo file_0 147 8 147 17.
-  Definition loc_431 : location_info := LocationInfo file_0 147 8 147 17.
-  Definition loc_432 : location_info := LocationInfo file_0 147 8 147 12.
-  Definition loc_433 : location_info := LocationInfo file_0 147 8 147 12.
-  Definition loc_434 : location_info := LocationInfo file_0 147 21 147 32.
-  Definition loc_435 : location_info := LocationInfo file_0 147 30 147 31.
-  Definition loc_436 : location_info := LocationInfo file_0 146 24 146 46.
-  Definition loc_437 : location_info := LocationInfo file_0 146 25 146 46.
-  Definition loc_438 : location_info := LocationInfo file_0 146 25 146 46.
-  Definition loc_439 : location_info := LocationInfo file_0 146 25 146 36.
-  Definition loc_440 : location_info := LocationInfo file_0 146 25 146 36.
-  Definition loc_441 : location_info := LocationInfo file_0 146 27 146 35.
-  Definition loc_442 : location_info := LocationInfo file_0 146 27 146 35.
-  Definition loc_443 : location_info := LocationInfo file_0 146 27 146 28.
-  Definition loc_444 : location_info := LocationInfo file_0 146 27 146 28.
-  Definition loc_445 : location_info := LocationInfo file_0 146 37 146 45.
-  Definition loc_446 : location_info := LocationInfo file_0 146 37 146 45.
-  Definition loc_449 : location_info := LocationInfo file_0 145 21 145 35.
-  Definition loc_452 : location_info := LocationInfo file_0 144 22 144 39.
-  Definition loc_453 : location_info := LocationInfo file_0 144 22 144 31.
-  Definition loc_454 : location_info := LocationInfo file_0 144 22 144 31.
-  Definition loc_455 : location_info := LocationInfo file_0 144 32 144 33.
-  Definition loc_456 : location_info := LocationInfo file_0 144 32 144 33.
-  Definition loc_457 : location_info := LocationInfo file_0 144 35 144 38.
-  Definition loc_458 : location_info := LocationInfo file_0 144 35 144 38.
-  Definition loc_461 : location_info := LocationInfo file_0 143 4 143 28.
-  Definition loc_462 : location_info := LocationInfo file_0 143 4 143 28.
-  Definition loc_463 : location_info := LocationInfo file_0 143 29 143 30.
-  Definition loc_464 : location_info := LocationInfo file_0 143 29 143 30.
-  Definition loc_467 : location_info := LocationInfo file_0 168 4 168 40.
-  Definition loc_468 : location_info := LocationInfo file_0 169 4 169 47.
-  Definition loc_469 : location_info := LocationInfo file_0 171 4 175 5.
-  Definition loc_470 : location_info := LocationInfo file_0 171 34 173 5.
-  Definition loc_471 : location_info := LocationInfo file_0 172 8 172 37.
-  Definition loc_472 : location_info := LocationInfo file_0 172 15 172 36.
-  Definition loc_473 : location_info := LocationInfo file_0 172 16 172 36.
-  Definition loc_474 : location_info := LocationInfo file_0 172 17 172 36.
-  Definition loc_475 : location_info := LocationInfo file_0 172 17 172 36.
-  Definition loc_476 : location_info := LocationInfo file_0 172 17 172 30.
-  Definition loc_477 : location_info := LocationInfo file_0 172 17 172 24.
-  Definition loc_478 : location_info := LocationInfo file_0 172 17 172 21.
-  Definition loc_479 : location_info := LocationInfo file_0 172 17 172 21.
-  Definition loc_480 : location_info := LocationInfo file_0 173 11 175 5.
-  Definition loc_481 : location_info := LocationInfo file_0 174 8 174 30.
-  Definition loc_482 : location_info := LocationInfo file_0 174 15 174 29.
-  Definition loc_483 : location_info := LocationInfo file_0 171 8 171 32.
-  Definition loc_484 : location_info := LocationInfo file_0 171 8 171 17.
-  Definition loc_485 : location_info := LocationInfo file_0 171 8 171 17.
-  Definition loc_486 : location_info := LocationInfo file_0 171 8 171 12.
-  Definition loc_487 : location_info := LocationInfo file_0 171 8 171 12.
-  Definition loc_488 : location_info := LocationInfo file_0 171 21 171 32.
-  Definition loc_489 : location_info := LocationInfo file_0 171 30 171 31.
-  Definition loc_490 : location_info := LocationInfo file_0 169 24 169 46.
-  Definition loc_491 : location_info := LocationInfo file_0 169 25 169 46.
-  Definition loc_492 : location_info := LocationInfo file_0 169 25 169 46.
-  Definition loc_493 : location_info := LocationInfo file_0 169 25 169 36.
-  Definition loc_494 : location_info := LocationInfo file_0 169 25 169 36.
-  Definition loc_495 : location_info := LocationInfo file_0 169 27 169 35.
-  Definition loc_496 : location_info := LocationInfo file_0 169 27 169 35.
-  Definition loc_497 : location_info := LocationInfo file_0 169 27 169 28.
-  Definition loc_498 : location_info := LocationInfo file_0 169 27 169 28.
-  Definition loc_499 : location_info := LocationInfo file_0 169 37 169 45.
-  Definition loc_500 : location_info := LocationInfo file_0 169 37 169 45.
-  Definition loc_503 : location_info := LocationInfo file_0 168 22 168 39.
-  Definition loc_504 : location_info := LocationInfo file_0 168 22 168 31.
-  Definition loc_505 : location_info := LocationInfo file_0 168 22 168 31.
-  Definition loc_506 : location_info := LocationInfo file_0 168 32 168 33.
-  Definition loc_507 : location_info := LocationInfo file_0 168 32 168 33.
-  Definition loc_508 : location_info := LocationInfo file_0 168 35 168 38.
-  Definition loc_509 : location_info := LocationInfo file_0 168 35 168 38.
-  Definition loc_514 : location_info := LocationInfo file_0 187 4 187 40.
-  Definition loc_515 : location_info := LocationInfo file_0 188 4 188 47.
-  Definition loc_516 : location_info := LocationInfo file_0 190 4 197 5.
-  Definition loc_517 : location_info := LocationInfo file_0 190 34 195 5.
-  Definition loc_518 : location_info := LocationInfo file_0 191 8 191 38.
-  Definition loc_519 : location_info := LocationInfo file_0 192 8 192 32.
-  Definition loc_520 : location_info := LocationInfo file_0 193 8 193 36.
-  Definition loc_521 : location_info := LocationInfo file_0 194 8 194 23.
-  Definition loc_522 : location_info := LocationInfo file_0 194 15 194 22.
-  Definition loc_523 : location_info := LocationInfo file_0 194 15 194 22.
-  Definition loc_524 : location_info := LocationInfo file_0 193 8 193 29.
-  Definition loc_525 : location_info := LocationInfo file_0 193 8 193 25.
-  Definition loc_526 : location_info := LocationInfo file_0 193 8 193 15.
-  Definition loc_527 : location_info := LocationInfo file_0 193 8 193 12.
-  Definition loc_528 : location_info := LocationInfo file_0 193 8 193 12.
-  Definition loc_529 : location_info := LocationInfo file_0 193 32 193 35.
-  Definition loc_530 : location_info := LocationInfo file_0 193 32 193 35.
-  Definition loc_531 : location_info := LocationInfo file_0 192 8 192 17.
-  Definition loc_532 : location_info := LocationInfo file_0 192 8 192 12.
-  Definition loc_533 : location_info := LocationInfo file_0 192 8 192 12.
-  Definition loc_534 : location_info := LocationInfo file_0 192 20 192 31.
-  Definition loc_535 : location_info := LocationInfo file_0 192 29 192 30.
-  Definition loc_536 : location_info := LocationInfo file_0 191 8 191 15.
-  Definition loc_537 : location_info := LocationInfo file_0 191 18 191 37.
-  Definition loc_538 : location_info := LocationInfo file_0 191 18 191 37.
-  Definition loc_539 : location_info := LocationInfo file_0 191 18 191 31.
-  Definition loc_540 : location_info := LocationInfo file_0 191 18 191 25.
-  Definition loc_541 : location_info := LocationInfo file_0 191 18 191 22.
-  Definition loc_542 : location_info := LocationInfo file_0 191 18 191 22.
-  Definition loc_543 : location_info := LocationInfo file_0 195 11 197 5.
-  Definition loc_544 : location_info := LocationInfo file_0 196 8 196 30.
-  Definition loc_545 : location_info := LocationInfo file_0 196 15 196 29.
-  Definition loc_546 : location_info := LocationInfo file_0 190 8 190 32.
-  Definition loc_547 : location_info := LocationInfo file_0 190 8 190 17.
-  Definition loc_548 : location_info := LocationInfo file_0 190 8 190 17.
-  Definition loc_549 : location_info := LocationInfo file_0 190 8 190 12.
-  Definition loc_550 : location_info := LocationInfo file_0 190 8 190 12.
-  Definition loc_551 : location_info := LocationInfo file_0 190 21 190 32.
-  Definition loc_552 : location_info := LocationInfo file_0 190 30 190 31.
-  Definition loc_553 : location_info := LocationInfo file_0 188 24 188 46.
-  Definition loc_554 : location_info := LocationInfo file_0 188 25 188 46.
-  Definition loc_555 : location_info := LocationInfo file_0 188 25 188 46.
-  Definition loc_556 : location_info := LocationInfo file_0 188 25 188 36.
-  Definition loc_557 : location_info := LocationInfo file_0 188 25 188 36.
-  Definition loc_558 : location_info := LocationInfo file_0 188 27 188 35.
-  Definition loc_559 : location_info := LocationInfo file_0 188 27 188 35.
-  Definition loc_560 : location_info := LocationInfo file_0 188 27 188 28.
-  Definition loc_561 : location_info := LocationInfo file_0 188 27 188 28.
-  Definition loc_562 : location_info := LocationInfo file_0 188 37 188 45.
-  Definition loc_563 : location_info := LocationInfo file_0 188 37 188 45.
-  Definition loc_566 : location_info := LocationInfo file_0 187 22 187 39.
-  Definition loc_567 : location_info := LocationInfo file_0 187 22 187 31.
-  Definition loc_568 : location_info := LocationInfo file_0 187 22 187 31.
-  Definition loc_569 : location_info := LocationInfo file_0 187 32 187 33.
-  Definition loc_570 : location_info := LocationInfo file_0 187 32 187 33.
-  Definition loc_571 : location_info := LocationInfo file_0 187 35 187 38.
-  Definition loc_572 : location_info := LocationInfo file_0 187 35 187 38.
-  Definition loc_577 : location_info := LocationInfo file_0 207 2 207 11.
-  Definition loc_578 : location_info := LocationInfo file_0 207 9 207 10.
+  Definition loc_2 : location_info := LocationInfo file_0 219 2 221 3.
+  Definition loc_3 : location_info := LocationInfo file_0 223 2 223 89.
+  Definition loc_4 : location_info := LocationInfo file_0 226 2 226 33.
+  Definition loc_5 : location_info := LocationInfo file_0 228 2 228 25.
+  Definition loc_6 : location_info := LocationInfo file_0 236 2 241 3.
+  Definition loc_7 : location_info := LocationInfo file_0 236 2 241 3.
+  Definition loc_8 : location_info := LocationInfo file_0 236 2 241 3.
+  Definition loc_9 : location_info := LocationInfo file_0 242 2 242 55.
+  Definition loc_10 : location_info := LocationInfo file_0 243 2 243 10.
+  Definition loc_11 : location_info := LocationInfo file_0 243 2 243 4.
+  Definition loc_12 : location_info := LocationInfo file_0 243 3 243 4.
+  Definition loc_13 : location_info := LocationInfo file_0 243 3 243 4.
+  Definition loc_14 : location_info := LocationInfo file_0 243 7 243 9.
+  Definition loc_15 : location_info := LocationInfo file_0 243 7 243 9.
+  Definition loc_16 : location_info := LocationInfo file_0 242 2 242 12.
+  Definition loc_17 : location_info := LocationInfo file_0 242 2 242 12.
+  Definition loc_18 : location_info := LocationInfo file_0 242 13 242 32.
+  Definition loc_19 : location_info := LocationInfo file_0 242 34 242 43.
+  Definition loc_20 : location_info := LocationInfo file_0 242 34 242 43.
+  Definition loc_21 : location_info := LocationInfo file_0 242 34 242 35.
+  Definition loc_22 : location_info := LocationInfo file_0 242 34 242 35.
+  Definition loc_23 : location_info := LocationInfo file_0 242 45 242 53.
+  Definition loc_24 : location_info := LocationInfo file_0 242 45 242 53.
+  Definition loc_25 : location_info := LocationInfo file_0 242 45 242 46.
+  Definition loc_26 : location_info := LocationInfo file_0 242 45 242 46.
+  Definition loc_27 : location_info := LocationInfo file_0 236 43 241 3.
+  Definition loc_28 : location_info := LocationInfo file_0 237 4 239 5.
+  Definition loc_29 : location_info := LocationInfo file_0 240 4 240 17.
+  Definition loc_30 : location_info := LocationInfo file_0 240 17 240 5.
+  Definition loc_31 : location_info := LocationInfo file_0 236 2 241 3.
+  Definition loc_33 : location_info := LocationInfo file_0 236 35 236 36.
+  Definition loc_34 : location_info := LocationInfo file_0 236 35 236 41.
+  Definition loc_35 : location_info := LocationInfo file_0 236 35 236 36.
+  Definition loc_36 : location_info := LocationInfo file_0 236 35 236 36.
+  Definition loc_37 : location_info := LocationInfo file_0 236 40 236 41.
+  Definition loc_38 : location_info := LocationInfo file_0 240 4 240 16.
+  Definition loc_39 : location_info := LocationInfo file_0 240 5 240 16.
+  Definition loc_40 : location_info := LocationInfo file_0 240 6 240 8.
+  Definition loc_41 : location_info := LocationInfo file_0 237 42 239 5.
+  Definition loc_42 : location_info := LocationInfo file_0 238 6 238 80.
+  Definition loc_43 : location_info := LocationInfo file_0 238 6 238 16.
+  Definition loc_44 : location_info := LocationInfo file_0 238 6 238 16.
+  Definition loc_45 : location_info := LocationInfo file_0 238 17 238 20.
+  Definition loc_46 : location_info := LocationInfo file_0 238 18 238 20.
+  Definition loc_47 : location_info := LocationInfo file_0 238 22 238 48.
+  Definition loc_48 : location_info := LocationInfo file_0 238 22 238 48.
+  Definition loc_49 : location_info := LocationInfo file_0 238 22 238 44.
+  Definition loc_50 : location_info := LocationInfo file_0 238 22 238 38.
+  Definition loc_51 : location_info := LocationInfo file_0 238 22 238 36.
+  Definition loc_52 : location_info := LocationInfo file_0 238 22 238 36.
+  Definition loc_53 : location_info := LocationInfo file_0 238 22 238 33.
+  Definition loc_54 : location_info := LocationInfo file_0 238 22 238 33.
+  Definition loc_55 : location_info := LocationInfo file_0 238 24 238 32.
+  Definition loc_56 : location_info := LocationInfo file_0 238 24 238 32.
+  Definition loc_57 : location_info := LocationInfo file_0 238 24 238 25.
+  Definition loc_58 : location_info := LocationInfo file_0 238 24 238 25.
+  Definition loc_59 : location_info := LocationInfo file_0 238 34 238 35.
+  Definition loc_60 : location_info := LocationInfo file_0 238 34 238 35.
+  Definition loc_61 : location_info := LocationInfo file_0 238 50 238 78.
+  Definition loc_62 : location_info := LocationInfo file_0 238 50 238 78.
+  Definition loc_63 : location_info := LocationInfo file_0 238 50 238 72.
+  Definition loc_64 : location_info := LocationInfo file_0 238 50 238 66.
+  Definition loc_65 : location_info := LocationInfo file_0 238 50 238 64.
+  Definition loc_66 : location_info := LocationInfo file_0 238 50 238 64.
+  Definition loc_67 : location_info := LocationInfo file_0 238 50 238 61.
+  Definition loc_68 : location_info := LocationInfo file_0 238 50 238 61.
+  Definition loc_69 : location_info := LocationInfo file_0 238 52 238 60.
+  Definition loc_70 : location_info := LocationInfo file_0 238 52 238 60.
+  Definition loc_71 : location_info := LocationInfo file_0 238 52 238 53.
+  Definition loc_72 : location_info := LocationInfo file_0 238 52 238 53.
+  Definition loc_73 : location_info := LocationInfo file_0 238 62 238 63.
+  Definition loc_74 : location_info := LocationInfo file_0 238 62 238 63.
+  Definition loc_76 : location_info := LocationInfo file_0 237 7 237 40.
+  Definition loc_77 : location_info := LocationInfo file_0 237 7 237 25.
+  Definition loc_78 : location_info := LocationInfo file_0 237 7 237 25.
+  Definition loc_79 : location_info := LocationInfo file_0 237 7 237 21.
+  Definition loc_80 : location_info := LocationInfo file_0 237 7 237 21.
+  Definition loc_81 : location_info := LocationInfo file_0 237 7 237 18.
+  Definition loc_82 : location_info := LocationInfo file_0 237 7 237 18.
+  Definition loc_83 : location_info := LocationInfo file_0 237 9 237 17.
+  Definition loc_84 : location_info := LocationInfo file_0 237 9 237 17.
+  Definition loc_85 : location_info := LocationInfo file_0 237 9 237 10.
+  Definition loc_86 : location_info := LocationInfo file_0 237 9 237 10.
+  Definition loc_87 : location_info := LocationInfo file_0 237 19 237 20.
+  Definition loc_88 : location_info := LocationInfo file_0 237 19 237 20.
+  Definition loc_89 : location_info := LocationInfo file_0 237 29 237 40.
+  Definition loc_90 : location_info := LocationInfo file_0 237 38 237 39.
+  Definition loc_91 : location_info := LocationInfo file_0 236 20 236 33.
+  Definition loc_92 : location_info := LocationInfo file_0 236 20 236 21.
+  Definition loc_93 : location_info := LocationInfo file_0 236 20 236 21.
+  Definition loc_94 : location_info := LocationInfo file_0 236 24 236 33.
+  Definition loc_95 : location_info := LocationInfo file_0 236 24 236 33.
+  Definition loc_96 : location_info := LocationInfo file_0 236 24 236 25.
+  Definition loc_97 : location_info := LocationInfo file_0 236 24 236 25.
+  Definition loc_98 : location_info := LocationInfo file_0 236 17 236 18.
+  Definition loc_101 : location_info := LocationInfo file_0 228 2 228 10.
+  Definition loc_102 : location_info := LocationInfo file_0 228 2 228 10.
+  Definition loc_103 : location_info := LocationInfo file_0 228 11 228 14.
+  Definition loc_104 : location_info := LocationInfo file_0 228 12 228 14.
+  Definition loc_105 : location_info := LocationInfo file_0 228 16 228 23.
+  Definition loc_106 : location_info := LocationInfo file_0 228 16 228 23.
+  Definition loc_107 : location_info := LocationInfo file_0 226 19 226 32.
+  Definition loc_108 : location_info := LocationInfo file_0 226 19 226 28.
+  Definition loc_109 : location_info := LocationInfo file_0 226 19 226 28.
+  Definition loc_110 : location_info := LocationInfo file_0 226 19 226 20.
+  Definition loc_111 : location_info := LocationInfo file_0 226 19 226 20.
+  Definition loc_112 : location_info := LocationInfo file_0 226 31 226 32.
+  Definition loc_115 : location_info := LocationInfo file_0 223 68 223 70.
+  Definition loc_116 : location_info := LocationInfo file_0 223 76 223 89.
+  Definition loc_117 : location_info := LocationInfo file_0 223 78 223 87.
+  Definition loc_118 : location_info := LocationInfo file_0 223 78 223 87.
+  Definition loc_119 : location_info := LocationInfo file_0 223 86 223 87.
+  Definition loc_120 : location_info := LocationInfo file_0 223 78 223 87.
+  Definition loc_121 : location_info := LocationInfo file_0 223 78 223 87.
+  Definition loc_122 : location_info := LocationInfo file_0 223 84 223 85.
+  Definition loc_123 : location_info := LocationInfo file_0 223 5 223 66.
+  Definition loc_124 : location_info := LocationInfo file_0 223 5 223 14.
+  Definition loc_125 : location_info := LocationInfo file_0 223 5 223 14.
+  Definition loc_126 : location_info := LocationInfo file_0 223 5 223 6.
+  Definition loc_127 : location_info := LocationInfo file_0 223 5 223 6.
+  Definition loc_128 : location_info := LocationInfo file_0 223 17 223 66.
+  Definition loc_129 : location_info := LocationInfo file_0 223 17 223 61.
+  Definition loc_130 : location_info := LocationInfo file_0 223 17 223 39.
+  Definition loc_131 : location_info := LocationInfo file_0 223 17 223 35.
+  Definition loc_132 : location_info := LocationInfo file_0 223 38 223 39.
+  Definition loc_133 : location_info := LocationInfo file_0 223 42 223 61.
+  Definition loc_134 : location_info := LocationInfo file_0 223 64 223 66.
+  Definition loc_135 : location_info := LocationInfo file_0 219 47 221 3.
+  Definition loc_136 : location_info := LocationInfo file_0 220 4 220 11.
+  Definition loc_139 : location_info := LocationInfo file_0 219 5 219 45.
+  Definition loc_140 : location_info := LocationInfo file_0 219 5 219 33.
+  Definition loc_141 : location_info := LocationInfo file_0 219 5 219 22.
+  Definition loc_142 : location_info := LocationInfo file_0 219 5 219 22.
+  Definition loc_143 : location_info := LocationInfo file_0 219 23 219 32.
+  Definition loc_144 : location_info := LocationInfo file_0 219 23 219 32.
+  Definition loc_145 : location_info := LocationInfo file_0 219 23 219 24.
+  Definition loc_146 : location_info := LocationInfo file_0 219 23 219 24.
+  Definition loc_147 : location_info := LocationInfo file_0 219 37 219 45.
+  Definition loc_148 : location_info := LocationInfo file_0 219 37 219 45.
+  Definition loc_149 : location_info := LocationInfo file_0 219 37 219 38.
+  Definition loc_150 : location_info := LocationInfo file_0 219 37 219 38.
+  Definition loc_153 : location_info := LocationInfo file_0 78 2 78 56.
+  Definition loc_154 : location_info := LocationInfo file_0 79 2 79 18.
+  Definition loc_155 : location_info := LocationInfo file_0 80 2 80 21.
+  Definition loc_156 : location_info := LocationInfo file_0 81 2 81 17.
+  Definition loc_157 : location_info := LocationInfo file_0 89 2 92 3.
+  Definition loc_158 : location_info := LocationInfo file_0 89 6 89 11.
+  Definition loc_159 : location_info := LocationInfo file_0 89 2 92 3.
+  Definition loc_160 : location_info := LocationInfo file_0 89 30 92 3.
+  Definition loc_161 : location_info := LocationInfo file_0 90 4 90 37.
+  Definition loc_162 : location_info := LocationInfo file_0 91 4 91 37.
+  Definition loc_163 : location_info := LocationInfo file_0 89 2 92 3.
+  Definition loc_164 : location_info := LocationInfo file_0 89 22 89 28.
+  Definition loc_165 : location_info := LocationInfo file_0 89 22 89 23.
+  Definition loc_166 : location_info := LocationInfo file_0 89 22 89 28.
+  Definition loc_167 : location_info := LocationInfo file_0 89 22 89 23.
+  Definition loc_168 : location_info := LocationInfo file_0 89 22 89 23.
+  Definition loc_169 : location_info := LocationInfo file_0 89 27 89 28.
+  Definition loc_170 : location_info := LocationInfo file_0 91 4 91 32.
+  Definition loc_171 : location_info := LocationInfo file_0 91 4 91 26.
+  Definition loc_172 : location_info := LocationInfo file_0 91 4 91 20.
+  Definition loc_173 : location_info := LocationInfo file_0 91 4 91 18.
+  Definition loc_174 : location_info := LocationInfo file_0 91 4 91 18.
+  Definition loc_175 : location_info := LocationInfo file_0 91 4 91 15.
+  Definition loc_176 : location_info := LocationInfo file_0 91 4 91 15.
+  Definition loc_177 : location_info := LocationInfo file_0 91 6 91 14.
+  Definition loc_178 : location_info := LocationInfo file_0 91 6 91 14.
+  Definition loc_179 : location_info := LocationInfo file_0 91 6 91 7.
+  Definition loc_180 : location_info := LocationInfo file_0 91 6 91 7.
+  Definition loc_181 : location_info := LocationInfo file_0 91 16 91 17.
+  Definition loc_182 : location_info := LocationInfo file_0 91 16 91 17.
+  Definition loc_183 : location_info := LocationInfo file_0 91 35 91 36.
+  Definition loc_184 : location_info := LocationInfo file_0 90 4 90 22.
+  Definition loc_185 : location_info := LocationInfo file_0 90 4 90 18.
+  Definition loc_186 : location_info := LocationInfo file_0 90 4 90 18.
+  Definition loc_187 : location_info := LocationInfo file_0 90 4 90 15.
+  Definition loc_188 : location_info := LocationInfo file_0 90 4 90 15.
+  Definition loc_189 : location_info := LocationInfo file_0 90 6 90 14.
+  Definition loc_190 : location_info := LocationInfo file_0 90 6 90 14.
+  Definition loc_191 : location_info := LocationInfo file_0 90 6 90 7.
+  Definition loc_192 : location_info := LocationInfo file_0 90 6 90 7.
+  Definition loc_193 : location_info := LocationInfo file_0 90 16 90 17.
+  Definition loc_194 : location_info := LocationInfo file_0 90 16 90 17.
+  Definition loc_195 : location_info := LocationInfo file_0 90 25 90 36.
+  Definition loc_196 : location_info := LocationInfo file_0 90 34 90 35.
+  Definition loc_197 : location_info := LocationInfo file_0 89 13 89 20.
+  Definition loc_198 : location_info := LocationInfo file_0 89 13 89 14.
+  Definition loc_199 : location_info := LocationInfo file_0 89 13 89 14.
+  Definition loc_200 : location_info := LocationInfo file_0 89 17 89 20.
+  Definition loc_201 : location_info := LocationInfo file_0 89 17 89 20.
+  Definition loc_202 : location_info := LocationInfo file_0 89 6 89 7.
+  Definition loc_203 : location_info := LocationInfo file_0 89 10 89 11.
+  Definition loc_204 : location_info := LocationInfo file_0 81 2 81 10.
+  Definition loc_205 : location_info := LocationInfo file_0 81 2 81 3.
+  Definition loc_206 : location_info := LocationInfo file_0 81 2 81 3.
+  Definition loc_207 : location_info := LocationInfo file_0 81 13 81 16.
+  Definition loc_208 : location_info := LocationInfo file_0 81 13 81 16.
+  Definition loc_209 : location_info := LocationInfo file_0 80 2 80 10.
+  Definition loc_210 : location_info := LocationInfo file_0 80 2 80 3.
+  Definition loc_211 : location_info := LocationInfo file_0 80 2 80 3.
+  Definition loc_212 : location_info := LocationInfo file_0 80 13 80 20.
+  Definition loc_213 : location_info := LocationInfo file_0 80 13 80 20.
+  Definition loc_214 : location_info := LocationInfo file_0 79 2 79 11.
+  Definition loc_215 : location_info := LocationInfo file_0 79 2 79 3.
+  Definition loc_216 : location_info := LocationInfo file_0 79 2 79 3.
+  Definition loc_217 : location_info := LocationInfo file_0 79 14 79 17.
+  Definition loc_218 : location_info := LocationInfo file_0 79 14 79 17.
+  Definition loc_219 : location_info := LocationInfo file_0 78 18 78 55.
+  Definition loc_220 : location_info := LocationInfo file_0 78 18 78 29.
+  Definition loc_221 : location_info := LocationInfo file_0 78 18 78 29.
+  Definition loc_222 : location_info := LocationInfo file_0 78 30 78 49.
+  Definition loc_223 : location_info := LocationInfo file_0 78 51 78 54.
+  Definition loc_224 : location_info := LocationInfo file_0 78 51 78 54.
+  Definition loc_229 : location_info := LocationInfo file_0 103 4 103 21.
+  Definition loc_230 : location_info := LocationInfo file_0 103 11 103 20.
+  Definition loc_231 : location_info := LocationInfo file_0 103 11 103 14.
+  Definition loc_232 : location_info := LocationInfo file_0 103 11 103 14.
+  Definition loc_233 : location_info := LocationInfo file_0 103 17 103 20.
+  Definition loc_234 : location_info := LocationInfo file_0 103 17 103 20.
+  Definition loc_237 : location_info := LocationInfo file_0 116 4 116 55.
+  Definition loc_238 : location_info := LocationInfo file_0 122 4 131 5.
+  Definition loc_239 : location_info := LocationInfo file_0 122 4 131 5.
+  Definition loc_240 : location_info := LocationInfo file_0 122 13 131 5.
+  Definition loc_241 : location_info := LocationInfo file_0 123 8 125 9.
+  Definition loc_242 : location_info := LocationInfo file_0 126 8 128 9.
+  Definition loc_243 : location_info := LocationInfo file_0 129 8 129 22.
+  Definition loc_244 : location_info := LocationInfo file_0 129 22 129 9.
+  Definition loc_245 : location_info := LocationInfo file_0 130 8 130 46.
+  Definition loc_246 : location_info := LocationInfo file_0 122 4 131 5.
+  Definition loc_247 : location_info := LocationInfo file_0 122 4 131 5.
+  Definition loc_248 : location_info := LocationInfo file_0 130 8 130 16.
+  Definition loc_249 : location_info := LocationInfo file_0 130 19 130 45.
+  Definition loc_250 : location_info := LocationInfo file_0 130 19 130 33.
+  Definition loc_251 : location_info := LocationInfo file_0 130 20 130 28.
+  Definition loc_252 : location_info := LocationInfo file_0 130 20 130 28.
+  Definition loc_253 : location_info := LocationInfo file_0 130 31 130 32.
+  Definition loc_254 : location_info := LocationInfo file_0 130 36 130 45.
+  Definition loc_255 : location_info := LocationInfo file_0 130 36 130 45.
+  Definition loc_256 : location_info := LocationInfo file_0 130 36 130 37.
+  Definition loc_257 : location_info := LocationInfo file_0 130 36 130 37.
+  Definition loc_258 : location_info := LocationInfo file_0 129 8 129 21.
+  Definition loc_259 : location_info := LocationInfo file_0 129 8 129 17.
+  Definition loc_260 : location_info := LocationInfo file_0 129 8 129 17.
+  Definition loc_261 : location_info := LocationInfo file_0 129 8 129 9.
+  Definition loc_262 : location_info := LocationInfo file_0 129 8 129 9.
+  Definition loc_263 : location_info := LocationInfo file_0 129 20 129 21.
+  Definition loc_264 : location_info := LocationInfo file_0 126 97 128 9.
+  Definition loc_265 : location_info := LocationInfo file_0 127 12 127 28.
+  Definition loc_266 : location_info := LocationInfo file_0 127 19 127 27.
+  Definition loc_267 : location_info := LocationInfo file_0 127 19 127 27.
+  Definition loc_270 : location_info := LocationInfo file_0 126 11 126 51.
+  Definition loc_271 : location_info := LocationInfo file_0 126 11 126 36.
+  Definition loc_272 : location_info := LocationInfo file_0 126 11 126 36.
+  Definition loc_273 : location_info := LocationInfo file_0 126 11 126 32.
+  Definition loc_274 : location_info := LocationInfo file_0 126 11 126 32.
+  Definition loc_275 : location_info := LocationInfo file_0 126 11 126 22.
+  Definition loc_276 : location_info := LocationInfo file_0 126 11 126 22.
+  Definition loc_277 : location_info := LocationInfo file_0 126 13 126 21.
+  Definition loc_278 : location_info := LocationInfo file_0 126 13 126 21.
+  Definition loc_279 : location_info := LocationInfo file_0 126 13 126 14.
+  Definition loc_280 : location_info := LocationInfo file_0 126 13 126 14.
+  Definition loc_281 : location_info := LocationInfo file_0 126 23 126 31.
+  Definition loc_282 : location_info := LocationInfo file_0 126 23 126 31.
+  Definition loc_283 : location_info := LocationInfo file_0 126 40 126 51.
+  Definition loc_284 : location_info := LocationInfo file_0 126 49 126 50.
+  Definition loc_285 : location_info := LocationInfo file_0 126 55 126 95.
+  Definition loc_286 : location_info := LocationInfo file_0 126 55 126 88.
+  Definition loc_287 : location_info := LocationInfo file_0 126 55 126 88.
+  Definition loc_288 : location_info := LocationInfo file_0 126 55 126 84.
+  Definition loc_289 : location_info := LocationInfo file_0 126 55 126 78.
+  Definition loc_290 : location_info := LocationInfo file_0 126 55 126 76.
+  Definition loc_291 : location_info := LocationInfo file_0 126 55 126 76.
+  Definition loc_292 : location_info := LocationInfo file_0 126 55 126 66.
+  Definition loc_293 : location_info := LocationInfo file_0 126 55 126 66.
+  Definition loc_294 : location_info := LocationInfo file_0 126 57 126 65.
+  Definition loc_295 : location_info := LocationInfo file_0 126 57 126 65.
+  Definition loc_296 : location_info := LocationInfo file_0 126 57 126 58.
+  Definition loc_297 : location_info := LocationInfo file_0 126 57 126 58.
+  Definition loc_298 : location_info := LocationInfo file_0 126 67 126 75.
+  Definition loc_299 : location_info := LocationInfo file_0 126 67 126 75.
+  Definition loc_300 : location_info := LocationInfo file_0 126 92 126 95.
+  Definition loc_301 : location_info := LocationInfo file_0 126 92 126 95.
+  Definition loc_302 : location_info := LocationInfo file_0 123 147 125 9.
+  Definition loc_303 : location_info := LocationInfo file_0 124 12 124 28.
+  Definition loc_304 : location_info := LocationInfo file_0 124 19 124 27.
+  Definition loc_305 : location_info := LocationInfo file_0 124 19 124 27.
+  Definition loc_308 : location_info := LocationInfo file_0 123 11 123 51.
+  Definition loc_309 : location_info := LocationInfo file_0 123 11 123 36.
+  Definition loc_310 : location_info := LocationInfo file_0 123 11 123 36.
+  Definition loc_311 : location_info := LocationInfo file_0 123 11 123 32.
+  Definition loc_312 : location_info := LocationInfo file_0 123 11 123 32.
+  Definition loc_313 : location_info := LocationInfo file_0 123 11 123 22.
+  Definition loc_314 : location_info := LocationInfo file_0 123 11 123 22.
+  Definition loc_315 : location_info := LocationInfo file_0 123 13 123 21.
+  Definition loc_316 : location_info := LocationInfo file_0 123 13 123 21.
+  Definition loc_317 : location_info := LocationInfo file_0 123 13 123 14.
+  Definition loc_318 : location_info := LocationInfo file_0 123 13 123 14.
+  Definition loc_319 : location_info := LocationInfo file_0 123 23 123 31.
+  Definition loc_320 : location_info := LocationInfo file_0 123 23 123 31.
+  Definition loc_321 : location_info := LocationInfo file_0 123 40 123 51.
+  Definition loc_322 : location_info := LocationInfo file_0 123 49 123 50.
+  Definition loc_324 : location_info := LocationInfo file_0 123 56 123 96.
+  Definition loc_325 : location_info := LocationInfo file_0 123 56 123 81.
+  Definition loc_326 : location_info := LocationInfo file_0 123 56 123 81.
+  Definition loc_327 : location_info := LocationInfo file_0 123 56 123 77.
+  Definition loc_328 : location_info := LocationInfo file_0 123 56 123 77.
+  Definition loc_329 : location_info := LocationInfo file_0 123 56 123 67.
+  Definition loc_330 : location_info := LocationInfo file_0 123 56 123 67.
+  Definition loc_331 : location_info := LocationInfo file_0 123 58 123 66.
+  Definition loc_332 : location_info := LocationInfo file_0 123 58 123 66.
+  Definition loc_333 : location_info := LocationInfo file_0 123 58 123 59.
+  Definition loc_334 : location_info := LocationInfo file_0 123 58 123 59.
+  Definition loc_335 : location_info := LocationInfo file_0 123 68 123 76.
+  Definition loc_336 : location_info := LocationInfo file_0 123 68 123 76.
+  Definition loc_337 : location_info := LocationInfo file_0 123 85 123 96.
+  Definition loc_338 : location_info := LocationInfo file_0 123 94 123 95.
+  Definition loc_339 : location_info := LocationInfo file_0 123 100 123 144.
+  Definition loc_340 : location_info := LocationInfo file_0 123 100 123 137.
+  Definition loc_341 : location_info := LocationInfo file_0 123 100 123 137.
+  Definition loc_342 : location_info := LocationInfo file_0 123 100 123 133.
+  Definition loc_343 : location_info := LocationInfo file_0 123 100 123 123.
+  Definition loc_344 : location_info := LocationInfo file_0 123 100 123 121.
+  Definition loc_345 : location_info := LocationInfo file_0 123 100 123 121.
+  Definition loc_346 : location_info := LocationInfo file_0 123 100 123 111.
+  Definition loc_347 : location_info := LocationInfo file_0 123 100 123 111.
+  Definition loc_348 : location_info := LocationInfo file_0 123 102 123 110.
+  Definition loc_349 : location_info := LocationInfo file_0 123 102 123 110.
+  Definition loc_350 : location_info := LocationInfo file_0 123 102 123 103.
+  Definition loc_351 : location_info := LocationInfo file_0 123 102 123 103.
+  Definition loc_352 : location_info := LocationInfo file_0 123 112 123 120.
+  Definition loc_353 : location_info := LocationInfo file_0 123 112 123 120.
+  Definition loc_354 : location_info := LocationInfo file_0 123 141 123 144.
+  Definition loc_355 : location_info := LocationInfo file_0 123 141 123 144.
+  Definition loc_356 : location_info := LocationInfo file_0 122 10 122 11.
+  Definition loc_357 : location_info := LocationInfo file_0 116 22 116 54.
+  Definition loc_358 : location_info := LocationInfo file_0 116 22 116 38.
+  Definition loc_359 : location_info := LocationInfo file_0 116 22 116 38.
+  Definition loc_360 : location_info := LocationInfo file_0 116 39 116 48.
+  Definition loc_361 : location_info := LocationInfo file_0 116 39 116 48.
+  Definition loc_362 : location_info := LocationInfo file_0 116 39 116 40.
+  Definition loc_363 : location_info := LocationInfo file_0 116 39 116 40.
+  Definition loc_364 : location_info := LocationInfo file_0 116 50 116 53.
+  Definition loc_365 : location_info := LocationInfo file_0 116 50 116 53.
+  Definition loc_370 : location_info := LocationInfo file_0 144 4 144 32.
+  Definition loc_371 : location_info := LocationInfo file_0 145 4 145 40.
+  Definition loc_372 : location_info := LocationInfo file_0 146 4 146 36.
+  Definition loc_373 : location_info := LocationInfo file_0 147 4 147 47.
+  Definition loc_374 : location_info := LocationInfo file_0 148 4 152 5.
+  Definition loc_375 : location_info := LocationInfo file_0 154 4 154 28.
+  Definition loc_376 : location_info := LocationInfo file_0 155 4 155 28.
+  Definition loc_377 : location_info := LocationInfo file_0 156 4 156 32.
+  Definition loc_378 : location_info := LocationInfo file_0 158 4 158 20.
+  Definition loc_379 : location_info := LocationInfo file_0 158 11 158 19.
+  Definition loc_380 : location_info := LocationInfo file_0 158 11 158 19.
+  Definition loc_381 : location_info := LocationInfo file_0 156 4 156 23.
+  Definition loc_382 : location_info := LocationInfo file_0 156 4 156 17.
+  Definition loc_383 : location_info := LocationInfo file_0 156 4 156 11.
+  Definition loc_384 : location_info := LocationInfo file_0 156 4 156 8.
+  Definition loc_385 : location_info := LocationInfo file_0 156 4 156 8.
+  Definition loc_386 : location_info := LocationInfo file_0 156 26 156 31.
+  Definition loc_387 : location_info := LocationInfo file_0 156 26 156 31.
+  Definition loc_388 : location_info := LocationInfo file_0 155 4 155 21.
+  Definition loc_389 : location_info := LocationInfo file_0 155 4 155 17.
+  Definition loc_390 : location_info := LocationInfo file_0 155 4 155 11.
+  Definition loc_391 : location_info := LocationInfo file_0 155 4 155 8.
+  Definition loc_392 : location_info := LocationInfo file_0 155 4 155 8.
+  Definition loc_393 : location_info := LocationInfo file_0 155 24 155 27.
+  Definition loc_394 : location_info := LocationInfo file_0 155 24 155 27.
+  Definition loc_395 : location_info := LocationInfo file_0 154 4 154 13.
+  Definition loc_396 : location_info := LocationInfo file_0 154 4 154 8.
+  Definition loc_397 : location_info := LocationInfo file_0 154 4 154 8.
+  Definition loc_398 : location_info := LocationInfo file_0 154 16 154 27.
+  Definition loc_399 : location_info := LocationInfo file_0 154 25 154 26.
+  Definition loc_400 : location_info := LocationInfo file_0 148 34 150 5.
+  Definition loc_401 : location_info := LocationInfo file_0 149 8 149 39.
+  Definition loc_402 : location_info := LocationInfo file_0 149 8 149 16.
+  Definition loc_403 : location_info := LocationInfo file_0 149 19 149 38.
+  Definition loc_404 : location_info := LocationInfo file_0 149 19 149 38.
+  Definition loc_405 : location_info := LocationInfo file_0 149 19 149 32.
+  Definition loc_406 : location_info := LocationInfo file_0 149 19 149 26.
+  Definition loc_407 : location_info := LocationInfo file_0 149 19 149 23.
+  Definition loc_408 : location_info := LocationInfo file_0 149 19 149 23.
+  Definition loc_409 : location_info := LocationInfo file_0 150 11 152 5.
+  Definition loc_410 : location_info := LocationInfo file_0 150 40 152 5.
+  Definition loc_411 : location_info := LocationInfo file_0 151 6 151 20.
+  Definition loc_412 : location_info := LocationInfo file_0 151 6 151 14.
+  Definition loc_413 : location_info := LocationInfo file_0 151 6 151 7.
+  Definition loc_414 : location_info := LocationInfo file_0 151 6 151 7.
+  Definition loc_415 : location_info := LocationInfo file_0 151 6 151 19.
+  Definition loc_416 : location_info := LocationInfo file_0 151 6 151 14.
+  Definition loc_417 : location_info := LocationInfo file_0 151 6 151 14.
+  Definition loc_418 : location_info := LocationInfo file_0 151 6 151 7.
+  Definition loc_419 : location_info := LocationInfo file_0 151 6 151 7.
+  Definition loc_420 : location_info := LocationInfo file_0 151 18 151 19.
+  Definition loc_422 : location_info := LocationInfo file_0 150 14 150 38.
+  Definition loc_423 : location_info := LocationInfo file_0 150 14 150 23.
+  Definition loc_424 : location_info := LocationInfo file_0 150 14 150 23.
+  Definition loc_425 : location_info := LocationInfo file_0 150 14 150 18.
+  Definition loc_426 : location_info := LocationInfo file_0 150 14 150 18.
+  Definition loc_427 : location_info := LocationInfo file_0 150 27 150 38.
+  Definition loc_428 : location_info := LocationInfo file_0 150 36 150 37.
+  Definition loc_429 : location_info := LocationInfo file_0 148 8 148 32.
+  Definition loc_430 : location_info := LocationInfo file_0 148 8 148 17.
+  Definition loc_431 : location_info := LocationInfo file_0 148 8 148 17.
+  Definition loc_432 : location_info := LocationInfo file_0 148 8 148 12.
+  Definition loc_433 : location_info := LocationInfo file_0 148 8 148 12.
+  Definition loc_434 : location_info := LocationInfo file_0 148 21 148 32.
+  Definition loc_435 : location_info := LocationInfo file_0 148 30 148 31.
+  Definition loc_436 : location_info := LocationInfo file_0 147 24 147 46.
+  Definition loc_437 : location_info := LocationInfo file_0 147 25 147 46.
+  Definition loc_438 : location_info := LocationInfo file_0 147 25 147 46.
+  Definition loc_439 : location_info := LocationInfo file_0 147 25 147 36.
+  Definition loc_440 : location_info := LocationInfo file_0 147 25 147 36.
+  Definition loc_441 : location_info := LocationInfo file_0 147 27 147 35.
+  Definition loc_442 : location_info := LocationInfo file_0 147 27 147 35.
+  Definition loc_443 : location_info := LocationInfo file_0 147 27 147 28.
+  Definition loc_444 : location_info := LocationInfo file_0 147 27 147 28.
+  Definition loc_445 : location_info := LocationInfo file_0 147 37 147 45.
+  Definition loc_446 : location_info := LocationInfo file_0 147 37 147 45.
+  Definition loc_449 : location_info := LocationInfo file_0 146 21 146 35.
+  Definition loc_452 : location_info := LocationInfo file_0 145 22 145 39.
+  Definition loc_453 : location_info := LocationInfo file_0 145 22 145 31.
+  Definition loc_454 : location_info := LocationInfo file_0 145 22 145 31.
+  Definition loc_455 : location_info := LocationInfo file_0 145 32 145 33.
+  Definition loc_456 : location_info := LocationInfo file_0 145 32 145 33.
+  Definition loc_457 : location_info := LocationInfo file_0 145 35 145 38.
+  Definition loc_458 : location_info := LocationInfo file_0 145 35 145 38.
+  Definition loc_461 : location_info := LocationInfo file_0 144 4 144 28.
+  Definition loc_462 : location_info := LocationInfo file_0 144 4 144 28.
+  Definition loc_463 : location_info := LocationInfo file_0 144 29 144 30.
+  Definition loc_464 : location_info := LocationInfo file_0 144 29 144 30.
+  Definition loc_467 : location_info := LocationInfo file_0 169 4 169 40.
+  Definition loc_468 : location_info := LocationInfo file_0 170 4 170 47.
+  Definition loc_469 : location_info := LocationInfo file_0 172 4 176 5.
+  Definition loc_470 : location_info := LocationInfo file_0 172 34 174 5.
+  Definition loc_471 : location_info := LocationInfo file_0 173 8 173 37.
+  Definition loc_472 : location_info := LocationInfo file_0 173 15 173 36.
+  Definition loc_473 : location_info := LocationInfo file_0 173 16 173 36.
+  Definition loc_474 : location_info := LocationInfo file_0 173 17 173 36.
+  Definition loc_475 : location_info := LocationInfo file_0 173 17 173 36.
+  Definition loc_476 : location_info := LocationInfo file_0 173 17 173 30.
+  Definition loc_477 : location_info := LocationInfo file_0 173 17 173 24.
+  Definition loc_478 : location_info := LocationInfo file_0 173 17 173 21.
+  Definition loc_479 : location_info := LocationInfo file_0 173 17 173 21.
+  Definition loc_480 : location_info := LocationInfo file_0 174 11 176 5.
+  Definition loc_481 : location_info := LocationInfo file_0 175 8 175 30.
+  Definition loc_482 : location_info := LocationInfo file_0 175 15 175 29.
+  Definition loc_483 : location_info := LocationInfo file_0 172 8 172 32.
+  Definition loc_484 : location_info := LocationInfo file_0 172 8 172 17.
+  Definition loc_485 : location_info := LocationInfo file_0 172 8 172 17.
+  Definition loc_486 : location_info := LocationInfo file_0 172 8 172 12.
+  Definition loc_487 : location_info := LocationInfo file_0 172 8 172 12.
+  Definition loc_488 : location_info := LocationInfo file_0 172 21 172 32.
+  Definition loc_489 : location_info := LocationInfo file_0 172 30 172 31.
+  Definition loc_490 : location_info := LocationInfo file_0 170 24 170 46.
+  Definition loc_491 : location_info := LocationInfo file_0 170 25 170 46.
+  Definition loc_492 : location_info := LocationInfo file_0 170 25 170 46.
+  Definition loc_493 : location_info := LocationInfo file_0 170 25 170 36.
+  Definition loc_494 : location_info := LocationInfo file_0 170 25 170 36.
+  Definition loc_495 : location_info := LocationInfo file_0 170 27 170 35.
+  Definition loc_496 : location_info := LocationInfo file_0 170 27 170 35.
+  Definition loc_497 : location_info := LocationInfo file_0 170 27 170 28.
+  Definition loc_498 : location_info := LocationInfo file_0 170 27 170 28.
+  Definition loc_499 : location_info := LocationInfo file_0 170 37 170 45.
+  Definition loc_500 : location_info := LocationInfo file_0 170 37 170 45.
+  Definition loc_503 : location_info := LocationInfo file_0 169 22 169 39.
+  Definition loc_504 : location_info := LocationInfo file_0 169 22 169 31.
+  Definition loc_505 : location_info := LocationInfo file_0 169 22 169 31.
+  Definition loc_506 : location_info := LocationInfo file_0 169 32 169 33.
+  Definition loc_507 : location_info := LocationInfo file_0 169 32 169 33.
+  Definition loc_508 : location_info := LocationInfo file_0 169 35 169 38.
+  Definition loc_509 : location_info := LocationInfo file_0 169 35 169 38.
+  Definition loc_514 : location_info := LocationInfo file_0 188 4 188 40.
+  Definition loc_515 : location_info := LocationInfo file_0 189 4 189 47.
+  Definition loc_516 : location_info := LocationInfo file_0 191 4 198 5.
+  Definition loc_517 : location_info := LocationInfo file_0 191 34 196 5.
+  Definition loc_518 : location_info := LocationInfo file_0 192 8 192 38.
+  Definition loc_519 : location_info := LocationInfo file_0 193 8 193 32.
+  Definition loc_520 : location_info := LocationInfo file_0 194 8 194 36.
+  Definition loc_521 : location_info := LocationInfo file_0 195 8 195 23.
+  Definition loc_522 : location_info := LocationInfo file_0 195 15 195 22.
+  Definition loc_523 : location_info := LocationInfo file_0 195 15 195 22.
+  Definition loc_524 : location_info := LocationInfo file_0 194 8 194 29.
+  Definition loc_525 : location_info := LocationInfo file_0 194 8 194 25.
+  Definition loc_526 : location_info := LocationInfo file_0 194 8 194 15.
+  Definition loc_527 : location_info := LocationInfo file_0 194 8 194 12.
+  Definition loc_528 : location_info := LocationInfo file_0 194 8 194 12.
+  Definition loc_529 : location_info := LocationInfo file_0 194 32 194 35.
+  Definition loc_530 : location_info := LocationInfo file_0 194 32 194 35.
+  Definition loc_531 : location_info := LocationInfo file_0 193 8 193 17.
+  Definition loc_532 : location_info := LocationInfo file_0 193 8 193 12.
+  Definition loc_533 : location_info := LocationInfo file_0 193 8 193 12.
+  Definition loc_534 : location_info := LocationInfo file_0 193 20 193 31.
+  Definition loc_535 : location_info := LocationInfo file_0 193 29 193 30.
+  Definition loc_536 : location_info := LocationInfo file_0 192 8 192 15.
+  Definition loc_537 : location_info := LocationInfo file_0 192 18 192 37.
+  Definition loc_538 : location_info := LocationInfo file_0 192 18 192 37.
+  Definition loc_539 : location_info := LocationInfo file_0 192 18 192 31.
+  Definition loc_540 : location_info := LocationInfo file_0 192 18 192 25.
+  Definition loc_541 : location_info := LocationInfo file_0 192 18 192 22.
+  Definition loc_542 : location_info := LocationInfo file_0 192 18 192 22.
+  Definition loc_543 : location_info := LocationInfo file_0 196 11 198 5.
+  Definition loc_544 : location_info := LocationInfo file_0 197 8 197 30.
+  Definition loc_545 : location_info := LocationInfo file_0 197 15 197 29.
+  Definition loc_546 : location_info := LocationInfo file_0 191 8 191 32.
+  Definition loc_547 : location_info := LocationInfo file_0 191 8 191 17.
+  Definition loc_548 : location_info := LocationInfo file_0 191 8 191 17.
+  Definition loc_549 : location_info := LocationInfo file_0 191 8 191 12.
+  Definition loc_550 : location_info := LocationInfo file_0 191 8 191 12.
+  Definition loc_551 : location_info := LocationInfo file_0 191 21 191 32.
+  Definition loc_552 : location_info := LocationInfo file_0 191 30 191 31.
+  Definition loc_553 : location_info := LocationInfo file_0 189 24 189 46.
+  Definition loc_554 : location_info := LocationInfo file_0 189 25 189 46.
+  Definition loc_555 : location_info := LocationInfo file_0 189 25 189 46.
+  Definition loc_556 : location_info := LocationInfo file_0 189 25 189 36.
+  Definition loc_557 : location_info := LocationInfo file_0 189 25 189 36.
+  Definition loc_558 : location_info := LocationInfo file_0 189 27 189 35.
+  Definition loc_559 : location_info := LocationInfo file_0 189 27 189 35.
+  Definition loc_560 : location_info := LocationInfo file_0 189 27 189 28.
+  Definition loc_561 : location_info := LocationInfo file_0 189 27 189 28.
+  Definition loc_562 : location_info := LocationInfo file_0 189 37 189 45.
+  Definition loc_563 : location_info := LocationInfo file_0 189 37 189 45.
+  Definition loc_566 : location_info := LocationInfo file_0 188 22 188 39.
+  Definition loc_567 : location_info := LocationInfo file_0 188 22 188 31.
+  Definition loc_568 : location_info := LocationInfo file_0 188 22 188 31.
+  Definition loc_569 : location_info := LocationInfo file_0 188 32 188 33.
+  Definition loc_570 : location_info := LocationInfo file_0 188 32 188 33.
+  Definition loc_571 : location_info := LocationInfo file_0 188 35 188 38.
+  Definition loc_572 : location_info := LocationInfo file_0 188 35 188 38.
+  Definition loc_577 : location_info := LocationInfo file_0 208 2 208 11.
+  Definition loc_578 : location_info := LocationInfo file_0 208 9 208 10.
 
   (* Definition of struct [empty]. *)
   Program Definition struct_empty := {|
diff --git a/examples/proofs/mutable_map/generated_proof_fsm_init.v b/examples/proofs/mutable_map/generated_proof_fsm_init.v
index c78b1381..224720df 100644
--- a/examples/proofs/mutable_map/generated_proof_fsm_init.v
+++ b/examples/proofs/mutable_map/generated_proof_fsm_init.v
@@ -20,7 +20,7 @@ Section proof_fsm_init.
         arg_len ◁ₗ (len @ (int (size_t))) ∗
         local_storage ◁ₗ uninit LPtr ∗
         local_i ◁ₗ (i @ (int (size_t))) ∗
-        arg_m ◁ₗ (m @ (&own (struct (struct_fixed_size_map) [@{type} &own (array_iterator (struct_item) (i) (len) (replicate i Empty `at_type` item) (uninit (struct_item)) (replicate (len - i)%nat (uninit (struct_item)))) ; len @ (int (size_t)) ; len @ (int (size_t)) ]))) ∗
+        arg_m ◁ₗ (m @ (&own (struct (struct_fixed_size_map) [@{type} &own (array (struct_item) (replicate i Empty `at_type` item ++ replicate (len - i)%nat (uninit (struct_item)))) ; len @ (int (size_t)) ; len @ (int (size_t)) ]))) ∗
         ⌜i <= len⌝
     ]> $
       ∅
@@ -33,8 +33,9 @@ Section proof_fsm_init.
       all: print_typesystem_goal "fsm_init" "#1".
     Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
     all: try by apply: fsm_invariant_init; solve_goal.
+    all: try by apply/list_subequiv_split; solve_goal.
     all: try by rewrite length_filter_replicate_True; solve_goal.
-    all: try by f_equal; solve_goal.
+    all: try by rewrite !replicate_O; solve_goal.
     all: print_sidecondition_goal "fsm_init".
   Qed.
 End proof_fsm_init.
diff --git a/examples/proofs/mutable_map/generated_proof_fsm_realloc_if_necessary.v b/examples/proofs/mutable_map/generated_proof_fsm_realloc_if_necessary.v
index e6d241f2..a68bd4b5 100644
--- a/examples/proofs/mutable_map/generated_proof_fsm_realloc_if_necessary.v
+++ b/examples/proofs/mutable_map/generated_proof_fsm_realloc_if_necessary.v
@@ -55,12 +55,7 @@ Section proof_fsm_realloc_if_necessary.
     all: try by apply: fsm_copy_entries_not_add; solve_goal.
     all: try by apply: fsm_copy_entries_add; solve_goal.
     all: try by apply: fsm_copy_entries_id; solve_goal.
-    all: try (apply list_subequiv_split; [solve_goal|]).
-    all: try rewrite !firstn_app !take_replicate !skipn_app !drop_replicate !replicate_length !fmap_drop !drop_drop -minus_n_n.
-    all: try split; f_equal.
-    all: try by f_equal; lia.
-    all: try have ->:(i - (i + 1) = 0)%nat by lia.
-    all: try by rewrite !firstn_O.
+    all: try by apply list_subequiv_split; [solve_goal|]; normalize_and_simpl_goal; try solve_goal; f_equal; solve_goal.
     all: print_sidecondition_goal "fsm_realloc_if_necessary".
   Qed.
 End proof_fsm_realloc_if_necessary.
diff --git a/theories/lang/base.v b/theories/lang/base.v
index b285da5c..bff815e5 100644
--- a/theories/lang/base.v
+++ b/theories/lang/base.v
@@ -117,6 +117,10 @@ Proof using Type*. move => ?. by apply: partial_alter_ext => ? <-. Qed.
 
 End theorems.
 
+Lemma replicate_O {A} (x : A) n:
+  n = 0%nat -> replicate n x = [].
+Proof. by move => ->. Qed.
+
 Global Instance set_unfold_replicate A (x y : A) n:
   SetUnfoldElemOf x (replicate n y) (x = y ∧ n ≠ 0%nat).
 Proof. constructor. apply elem_of_replicate. Qed.
diff --git a/theories/lithium/simpl_instances.v b/theories/lithium/simpl_instances.v
index b41bbd69..e37e2b63 100644
--- a/theories/lithium/simpl_instances.v
+++ b/theories/lithium/simpl_instances.v
@@ -286,12 +286,18 @@ Global Instance simpl_fmap_cons_impl {A B} (l : list A) l2 (f : A → B):
   SimplImplRel (=) true (f <$> l) (x :: l2) (λ T, ∀ x' l2', l = x' :: l2' → f x' = x → f <$> l2' = l2 → T).
 Proof. split; last naive_solver. intros ? ?%fmap_cons_inv. naive_solver. Qed.
 Global Instance simpl_fmap_app_and {A B} (l : list A) l1 l2 (f : A → B):
-  SimplAndRel (=) (f <$> l) (l1 ++ l2) (λ T, ∃ l1' l2', l = l1' ++ l2' ∧ f <$> l1' = l1 ∧ f <$> l2' = l2 ∧ T).
+  SimplAndRel (=) (f <$> l) (l1 ++ l2) (λ T, f <$> take (length l1) l = l1 ∧ f <$> drop (length l1) l = l2 ∧ T).
 Proof.
   split.
-  - move => [?[?[?[?[??]]]]]; subst. rewrite fmap_app. naive_solver.
-  - move => [/fmap_app_inv]. naive_solver.
+  - move => [Hl1 [Hl2 ?]]; subst. split => //.
+    rewrite -Hl1 -fmap_app fmap_length take_length_le ?take_drop //.
+    rewrite -Hl1 fmap_length take_length. lia.
+  - move => [/fmap_app_inv [? [? [? [? Hfmap]]]] ?]; subst.
+    by rewrite fmap_length take_app drop_app.
 Qed.
+Global Instance simpl_fmap_assume_inj_Unsafe {A B} (l1 l2 : list A) (f : A → B) `{!AssumeInj (=) (=) f}:
+  SimplAndUnsafe true (f <$> l1 = f <$> l2) (λ T, l1 = l2 ∧ T).
+Proof. move => T [-> ?]. naive_solver. Qed.
 
 Global Instance simpl_replicate_app_and {A} (l1 l2 : list A) x n:
   SimplAndRel (=) (replicate n x) (l1 ++ l2) (λ T, ∃ n', shelve_hint (n' ≤ n)%nat ∧ l1 = replicate n' x ∧ l2 = replicate (n - n') x ∧ T).
diff --git a/theories/typing/array.v b/theories/typing/array.v
index 418871db..0d9eb37f 100644
--- a/theories/typing/array.v
+++ b/theories/typing/array.v
@@ -198,81 +198,4 @@ Section type.
   Global Instance type_place_array_inst l β ly1 it v (tyv : mtype) tys ly2 K:
     TypedPlace (BinOpPCtx (PtrOffsetOp ly1) (IntOp it) v tyv :: K) l β (array ly2 tys):=
     λ T, i2p (type_place_array l β T ly1 it v tyv tys ly2 K).
-
-  (*** array iterator *)
-  Program Definition array_iterator (ly : layout) (i : nat) (len : nat) (tys1 : list type) (ty : type) (tys2 : list type) : type := {|
-    ty_own β l := ⌜i ≤ len⌝%nat ∗ ⌜length tys1 = i⌝ ∗ ⌜length tys2 = (len - i)%nat⌝ ∗ l ◁ₗ{β} array ly (<[i := ty]> (tys1 ++ tys2))
-  |}%I.
-  Next Obligation. iIntros (?????????). iDestruct 1 as (???) "Ha". do 3 iSplitR => //. by iApply ty_share. Qed.
-
-  Lemma simplify_goal_array_iterator_0 l β T ly len tys1 tys2 ty:
-    T (⌜tys1 = []⌝ ∗ ⌜length tys2 = len⌝ ∗ ⌜(0 < len)%nat → tys2 !! 0%nat = Some ty⌝ ∗ l ◁ₗ{β} array ly tys2) -∗
-      simplify_goal (l◁ₗ{β} array_iterator ly 0%nat len tys1 ty tys2) T.
-  Proof.
-    iIntros "HT". iExists _. iFrame. iIntros "[-> [<- [% [$ Ha]]]]".
-    repeat iSplit; try iPureIntro => //. lia. by rewrite -minus_n_O.
-    rewrite /= list_insert_id'; eauto.
-  Qed.
-  Global Instance simplify_goal_array_iterator_0_inst l β ly len tys1 tys2 ty:
-    SimplifyGoalPlace l β (array_iterator ly 0%nat len tys1 ty tys2)%I (Some 0%N) :=
-    λ T, i2p (simplify_goal_array_iterator_0 l β T ly len tys1 tys2 ty).
-
-  Lemma type_place_array_iterator l β T ly1 it v (tyv : mtype) (i : nat) len tys1 ty tys2 ly2 K:
-    ⌜i < len⌝%nat ∗ ⌜ly1 = ly2⌝ ∗ subsume (v ◁ᵥ tyv) (v ◁ᵥ i @ int it) (
-    typed_place K (l offset{ly2}ₗ i) β ty (λ l2 β2 ty2 typ, T l2 β2 ty2 (λ t, array_iterator ly2 i len tys1 (typ t) tys2))) -∗
-    typed_place (BinOpPCtx (PtrOffsetOp ly1) (IntOp it) v tyv :: K) l β (array_iterator ly2 i len tys1 ty tys2) T.
-  Proof.
-    iIntros "[% [<- HP]]" (Φ) "[% [<- [% [% Hl]]]] HΦ" => /=. iIntros "Hv".
-    (* TODO: this is the same as type_place_array. Figure out if we can reuse the proof. *)
-    iDestruct ("HP" with "Hv") as "[Hv HP]".
-    iDestruct (int_val_to_int_Some with "Hv") as %?.
-    iApply wp_ptr_offset => //. by apply val_to_of_loc. lia.
-    iIntros "!#". iExists _. iSplit => //.
-    iDestruct (big_sepL_insert_acc with "Hl") as "[Hl Hc]" => //.
-      by apply list_lookup_insert; rewrite app_length; lia.
-    iApply ("HP" with "Hl"). iIntros (l' ty2 β2 typ R) "Hl' Htyp HT".
-    iApply ("HΦ" with "Hl' [-HT] HT"). iIntros (ty') "Hl'".
-    iMod ("Htyp" with "Hl'") as "[? $]". repeat  iSplitR => //.
-    setoid_rewrite list_insert_insert. by iApply ("Hc").
-  Qed.
-  Global Instance type_place_array_iterator_inst l β ly1 it v (tyv : mtype) (i : nat) len tys1 ty tys2 ly2 K:
-    TypedPlace (BinOpPCtx (PtrOffsetOp ly1) (IntOp it) v tyv :: K) l β (array_iterator ly2 i len tys1 ty tys2) :=
-    λ T, i2p (type_place_array_iterator l β T ly1 it v tyv i len tys1 ty tys2 ly2 K).
-
-  Lemma subsume_array_iterator_next l β T i1 i2 len ly tys11 ty1 tys21 tys12 ty2 tys22 `{!CanSolve (i2 = S i1)}:
-    (∃ ty1', ⌜tys12 = tys11 ++ [ty1']⌝ ∗ ⌜length tys21 > 0⌝%nat ∗ ⌜tail tys21 = tys22⌝ ∗
-         ⌜(i2 < len)%nat → tys22 !! 0%nat = Some ty2⌝ ∗
-        subsume ((l offset{ly}ₗ i1) ◁ₗ{β} ty1) ((l offset{ly}ₗ i1) ◁ₗ{β} ty1') T) -∗
-    subsume (l ◁ₗ{β} array_iterator ly i1 len tys11 ty1 tys21) (l ◁ₗ{β} array_iterator ly i2 len tys12 ty2 tys22) T.
-  Proof.
-    unfold CanSolve in *; subst.
-    iDestruct 1 as (ty1' -> Htys21 <- Hty2) "Hsub". destruct tys21 as [|ty' tys21]; simpl in *. lia.
-    iDestruct 1 as (? <- Hlen) "Ha". rewrite insert_app_r_alt // -minus_n_n/=.
-    iDestruct (array_get_type (length tys11) with "Ha") as "[Hty1 Ha]". by rewrite lookup_app_r // -minus_n_n //.
-    iDestruct ("Hsub" with "Hty1") as "[Hty1 $]".
-    iSplit; [|iSplit]; [..|iSplit]; try iPureIntro; simpl in *. lia. by rewrite app_length /=; lia. lia.
-    iDestruct (array_put_type with "Hty1 Ha") as "Ha".
-    rewrite list_insert_insert insert_app_r_alt // insert_app_r_alt ?app_length /=; last lia.
-    rewrite  -minus_n_n/=. have -> : (S (length tys11) - (length tys11 + 1) = 0)%nat by lia.
-    destruct tys21 as [|ty'' tys21] => /=. by rewrite app_nil_r.
-    simpl in *. rewrite -app_assoc cons_middle.
-    by have [->]: Some ty'' = Some ty2 by eauto with lia.
-  Qed.
-  Global Instance subsume_array_iterator_next_inst l β i1 i2 len ly tys11 ty1 tys21 tys12 ty2 tys22 `{!CanSolve (i2 = S i1)}:
-    SubsumePlace l β (array_iterator ly i1 len tys11 ty1 tys21) (array_iterator ly i2 len tys12 ty2 tys22) :=
-    λ T, i2p (subsume_array_iterator_next l β T i1 i2 len ly tys11 ty1 tys21 tys12 ty2 tys22).
-
-  (* TODO: support not iterating until the end? *)
-  Lemma subsume_array_iterator_array l β T i len ly tys1 ty tys2 tys':
-    ⌜len ≤ i⌝%nat ∗ ⌜tys1 = tys'⌝ ∗ (⌜i = len⌝ -∗ T) -∗
-    subsume (l ◁ₗ{β} array_iterator ly i len tys1 ty tys2) (l ◁ₗ{β} array ly tys') T.
-  Proof.
-    iIntros "(%&->&HT)".
-    iDestruct 1 as (? <- Hlen) "Ha". iDestruct ("HT" with "[]") as "$". by iPureIntro; lia.
-    rewrite insert_app_r_alt // -minus_n_n/=.
-    destruct tys2; simpl in *. by rewrite app_nil_r. lia.
-  Qed.
-  Global Instance subsume_array_iterator_array_inst l β i len ly tys1 ty tys2 tys':
-    SubsumePlace l β (array_iterator ly i len tys1 ty tys2) (array ly tys') :=
-    λ T, i2p (subsume_array_iterator_array l β T i len ly tys1 ty tys2 tys').
 End type.
diff --git a/theories/typing/automation/normalize.v b/theories/typing/automation/normalize.v
index 8472e5b0..7123eee7 100644
--- a/theories/typing/automation/normalize.v
+++ b/theories/typing/automation/normalize.v
@@ -13,10 +13,13 @@ Lemma NatZmul_add_distr_r (n1 n2 : nat) z:
 Proof. lia. Qed.
 
 Hint Rewrite @drop_0 @take_ge using can_solve_tac : refinedc_rewrite.
+Hint Rewrite @take_app_le @drop_app_ge using can_solve_tac : refinedc_rewrite.
 Hint Rewrite @insert_length @app_length @fmap_length @rotate_length @replicate_length @drop_length : refinedc_rewrite.
+Hint Rewrite <- @fmap_take @fmap_drop : refinedc_rewrite.
 Hint Rewrite @list_insert_fold : refinedc_rewrite.
 Hint Rewrite @list_insert_insert : refinedc_rewrite.
-Hint Rewrite @tail_replicate : refinedc_rewrite.
+Hint Rewrite @drop_drop : refinedc_rewrite.
+Hint Rewrite @tail_replicate @take_replicate @drop_replicate : refinedc_rewrite.
 Hint Rewrite <- @app_assoc @cons_middle : refinedc_rewrite.
 Hint Rewrite @app_nil_r @rev_involutive : refinedc_rewrite.
 Hint Rewrite @list_fmap_insert : refinedc_rewrite.
-- 
GitLab